ATE 2011

1st Workshop


Automated Theory Engineering
(ATE 2011)

to be held at 31 July 2011, Wrocław, Poland
in conjunction with the 23rd International Conference on Automated Deduction

   scopetopicsinvited speakersprogrammeimportant datescall for papersubmissionprogramme committeeregistrationtravel and accomodationsponsors   


Theory engineering 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 is to present users with lightweight domain specific modelling languages, and to devolve the technical intricacies of analysis tasks as far as possible to tools that provide heavyweight automation.
The workshop brings together tool and theory developers with industrial engineers to exchange experiences and ideas that stimulate further tool developments and theory designs. A main goal is the creation of a repository of case studies that allows developers to test and improve their theories and tools.
ATE is the successor of an invitation-only event.


Theory engineering is relevant to the design of systems, programs,APIs, protocols, algorithms, design patterns, specification languages,programming languages and beyond. It involves technology such as ITP systems, ATP systems, SAT/SMT solvers, model checkers and decision procedures. Specific topics of the workshop include,but are not limited to:

  • qualitative and quantitative modelling and analysis
  • formal specification and verification
  • domain specific models, languages and solvers
  • theorem proving technology for theory engineering
  • integration of theories and tools
  • applications of mechanised reasoning to formal modelling
  • industrial case studies/experiences
We especially invite industrial contributions from the areas of network protocols and concurrent systems, but any submission onthe topics outlined is very welcome.

Invited Speakers


  9:00–10:00  J. Urban  An Overview of Methods for Large-Theory Automated Theory Proving (Invited Talk)
10:00–10:30 coffee break
10:30–12:30   M. Beeson
 J. Halcomb
 W. Mayer
 Inconsistencies in the Process Specification Language (PSL)
 H.-H. Dang
 B. Möller
 Simplifying Pointer Kleene Algebra
 P. James
 M. Roggenbach
 Designing Domain Specific Languages for Verification: First Steps
12:30–14:00 lunch break
14:00–15:30  T. Griffin  Do Formal Methodists have Bell-Shaped Heads? (Invited Talk)
 V. Naudžiūnas
 T. Griffin
 A Domain-Specific Language for the Specification of Path Algebras
15:30–16:00 coffee break
16:30–18:00   W. Guttmann
 G. Struth
 T. Weber
 A Repository for Tarski-Kleene Algebras
Automated Theorem Engineering: Discussion Session
19:00 workshop dinner

Important Dates

  • submission deadline: 29 April 2011
  • notification: 30 May 2011
  • final version: 1 July 2011
  • workshop: 31 July 2011

Call for Paper

The full call for papers can be found here.


Submission of papers for presentation at the workshop are now invited. Submissions are limited to 10 pages, but shorter extended abstracts are welcome. All papers will be reviewed by the programme committee, and a balanced programme will be selected based on relevance and technical soundness. Submissions must be in PDF using the LaTeX EasyChair-format. Accepted papers will be published as CEUR Workshop Proceedings. Submission is via EasyChair.
We expect that one author of every accepted paper will present their work at the workshop.

If quality and quantity of the submissions warrants this, we plan to publish a special issue of a recognized journal on the topic of the workshop.

Programme Committee

The workshop organizers are Peter Höfner, Annabelle McIver and Georg Struth. If you have any question about the workshop, please email the organizers.


Detailed information concerning the registration for the workshop will be added soon.

Travel and Accommodation

For information concerning travel and accommodation, we refer to the CADE-webpage.


 The University of Sheffield logo NICTA logo