=Paper=
{{Paper
|id=None
|storemode=property
|title=None
|pdfUrl=https://ceur-ws.org/Vol-760/preface.pdf
|volume=Vol-760
}}
==None==
<pdf width="1500px">https://ceur-ws.org/Vol-760/preface.pdf</pdf>
<pre>
Peter Höfner
Annabelle McIver
Georg Struth (eds.)




                                     1st Workshop
                                                       on
                      Automated Theory Engineering


                                          Wroc!law, Poland
                                             July 31, 2011



                                          Proceedings
                                           Preface
This volume contains the proceedings of the first Workshop on Automated Theory Engineer-
ing 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, algo-
rithms, design patterns, specification languages, programming languages and beyond. It in-
volves 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 Wodzyń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.

Sheffield and Sydney, July 2011                                                     Peter Höfner
                                                                                Annabelle McIver
                                                                                   Georg Struth
                                    Organisation


Programme Committee
Michael Butler                        University of Southampton, UK
Ewen Denney                           NASA, US
Peter Höfner                         NICTA, Australia
Joe Hurd                              Galois, Inc., US
Rajeev Joshi                          NASA (JPL), US
Annabelle McIver                      Macquarie University/NICTA, Australia
Stephan Merz                          INRIA, France
Marius Portmann                       University of Queensland/NICTA, Australia
Georg Struth                          University of Sheffield, UK
Geoff Sutcliffe                       University of Miami, US


Workshop Organisers
Peter Höfner                         NICTA, Australia
Annabelle McIver                      Macquarie University/NICTA, Australia
Georg Struth                          University of Sheffield, UK




Sponsors
NICTA, Australia
Department of Computer Science, The University of Sheffield, UK

</pre>