Proceedings This volume contains the proceedings of the first Workshop on Automated Theory Engineering which was held in Wroc!law, Poland, on July 31, 2011 as a satellite workshop of the 23rd International Conference on Automated Deduction (CADE).
Theory engineering, a term coined by Tony Hoare, means the development and mechanisation of mathematical axioms, definitions, theorems and inference procedures as needed to cover the essential concepts and analysis tasks of an application domain. It is essential for the qualitative and quantitative modelling and analysis of computing systems. The aim of theory engineering is to present users with domain specific modelling languages, and to devolve the technical intricacies of analysis tasks as far as possible to tools that provide heavyweight automation.
Theory engineering is relevant to the design of systems, programs, APIs, protocols, algorithms, design patterns, specification languages, programming languages and beyond. It involves technologies, such as interactive and automated theorem proving systems, satisfiability and satisfiability modulo theories solvers, model checkers and decision procedures.
The aim of this workshop was to bring together tool and theory developers with industrial engineers to exchange experiences and ideas that stimulate further tool developments and theory designs.
The diversity of topics relevant to theory engineering is reflected by the contributions to this volume. Each paper was refereed by at least three reviewers on its originality, technical soundness, quality of presentation and relevance to the workshop. The programme included two invited lectures by experts in the area: “An Overview of Methods for Large-Theory Automated Theorem Proving” by Josef Urban (Radboud University, The Netherlands), and “Do Formal Methodists have Bell-Shaped Heads?” by Timothy G. Griffin (University of Cambridge, UK).
We would like to thank our colleagues without whose help and support the workshop would not have been possible. First, Aaron Stump, the CADE workshop and tutorial chair and the local organisers Hans de Nivelle, Katarzyna Wodzyn´ska and Tomasz Wierzbicki for all their help. Second, the authors who supported this workshop by submitting papers and the two invited speakers for their contributions. Third, the members of the Programme Committee for carefully reviewing and selecting the papers. Finally, it is our pleasure to acknowledge the generous financial support by NICTA and the Department of Computer Science of the University of Sheffield.
Organisation
NASA (JPL), US Macquarie University/NICTA, Australia INRIA, France University of Queensland/NICTA, Australia University of Sheffield, UK University of Miami, US