ATE 2011
1st Workshop
on
Automated Theory Engineering
(ATE 2011)
http://www.nicta.com.au/ate2011/
to be held at 31 July 2011, Wrocław, Poland
in conjunction with the 23rd International Conference on Automated Deduction
| scope | topics | invited speakers | programme | important dates | call for paper | submission | programme committee | registration | travel and accomodation | sponsors |
Scope
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.
Topics
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
Invited Speakers
- Timothy Griffin, University of Cambridge, UK
- Josef Urban, Radboud University, The Netherlands
Programme
| 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
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
- 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
Registration
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.
http://cade23.ii.uni.wroc.pl/accomodation/
Sponsors
 |  |