This Workshop on Automated Theory eXploration will be held in June/July in Manchester, UK. It is associated with the 6th International Conference on Automated Reasoning (IJCAR) and follows on from two series of workshops: Automated Theory Engineering and Automatheo.
- mechanised reasoning for modelling and analysis
- automation applied to formal specification and verification
- domain specific models, languages and solvers
- theorem proving technology for theory exploration
- integration of theories and tools
- the formalisation and automation of mathematics
- case studies/experiences
- automated identification of key concepts and results
- supporting collaborative theory exploration
The first day of the workshop programme will be joint with WING 2012. ATX talks are in darker color. Each ATX talk is expected to last 25 minutes, leaving 5 minutes for questions.
| Saturday, June 30th | |
|---|---|
9:00 - 10:00 |
Invited Talk: Robert L. Constable, Cornell University: "Proof Assistants and the Dynamic Nature of Formal Theories" |
| Coffee break | |
| 10:30 - 12:00 | Daniel Larraz, Enric Rodriguez-Carbonell, and Albert Rubi: "SMT-Based Array Invariant Generation" |
| Pierre-Loic Garoche, Temesghen Kahsai, and Cesare Tinelli: "Invariant Stream Generators using Automatic Abstract Transformers based on a Decidable Logic" | |
| Roy McCasland: "Automated Theorem Discovery: a Case Study" | |
| Juan Pablo Galeotti and Andreas Zeller: "Inferring Loop Invariants Dynamically" | |
| Lunch break | |
| 13:30 - 15:00 | Friedrich Gretz, Joost-Pieter Katoen, and Annabelle McIver: "Prinsys – A Software Tool for the Synthesis of Probabilistic Invariants" |
| Yuhui Lin, Alan Bundy and Gudmund Grov: "The Use of Rippling to Automate Event-B Invariant Preservation Proofs" | |
| Rajiv Murali and Andrew Ireland: "E-SPARK: Automated Generation of Verifiable Code from Formally Verified Designs" | |
| Alexei Iliasov: "Augmenting formal development with use case reasoning" | |
| Coffee break | |
| 15:30 - 17:30 | Antoine Mine: "Invited Astree tutorial and paper: Abstract Domains for Bit-Level Machine Integer and Floating-point Operations" |
| Ott Tinn: "Faster Automatic Test Case Generation" | |
| Lamia Labed Jilani, Wided Ghardallou, Ali Mili: "Conclusive Proofs of While Loops Using Invariant Relations" | |
| Mengjun Li: "Formal Characterization and Verification of Loop Invariant Based on Finite Difference" | |
| Sunday, July 1st | |
|---|---|
9:00 - 10:00 |
Alan Smaill: "Theory Exploration: a role for Model Theory?" |
| Koen Claessen, Moa Johansson, Dan Rosen, and Nick Smallbone: "HipSpec : Automating Inductive Proofs of Program Properties" | |
| Coffee break | |
| 10:30 - 12:00 | René Neumann: "A Framework for Verified Depth-First Algorithms" |
| Jesse Alama: "Tipi: A TPTP-based theory development environment emphasizing proof analysis" | |
| Mark Adams and David Aspinall: "Recording and Refactoring HOL Light Tactic Proofs" | |
| Lunch break | |
| 13:30 - 14:30 | Alex Merry and Matvey Soloviev: "Rewriting Pattern Graphs" |
| Aleks Kissinger: "Synthesising Graphical Theories" | |
- Research papers, up to 10 pages;
- System/tool descriptions, up to 5 pages;
- Extended abstracts, up to 3 pages.
Research and tool papers must be unpublished and not submitted for publication elsewhere. Extended abstracts are intended to discuss ideas and work in progress. All papers will be reviewed by the programme committee.
Submissions must be in PDF using the LaTeX EasyChair-format http://www.easychair.org/easychair.zip. One author of each accepted submission is expected to present the paper at the conference. Associated systems demos are encouraged, where appropriate.
Please upload your submission at:
Accepted research and tool papers will be published as CEUR Workshop Proceedings.
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.
Submission: 3 April 2012- Submission: 17 April 2012 (Extended Deadline)
Notification: 8 May, 2012- Notification: 18 May, 2012
Final version: 5 June, 2012- Final version: 10 June, 2012
- Workshop: 30 June & 1 July, 2012
- Jacques Fleuriot (University of Edinburgh, UK)
- Timothy Griffin (University of Cambridge, UK)
- Peter Höfner (NICTA, Australia)
- Joe Hurd (Galois, USA)
- Temur Kutsia (RISC, Austria)
- Roy McCasland (University of Edinburgh, UK)
- Annabelle McIver (Macquarie University, Australia)
- Stephan Merz (INRIA, France)
- Petros Papapanagiotou (University of Edinburgh, UK)
- Alan Smaill (University of Edinburgh, UK)
- David Stanovsky (Charles University, Czech Republic)
- Georg Struth (University of Sheffield, UK)
- Josef Urban (Radboud University, Netherlands)
ATX 2012 is a merger of the ATE and Automatheo workshops:
ATE (International Workshop on Automated Theory Engineering) focuses on 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. This 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.
Automatheo (Workshop on Automated Mathematical Theory Exploration) aims to highlight the area of mathematical theory exploration, an exciting emerging research topic for mathematicians, developers of formalised mathematics, and those working on verified software. This topic concerns the theory and practice of developing software systems that support the automated development of mathematical theories, including the invention of definitions, theorems, conjectures, problems, examples and algorithms. The workshop aims to highlight the research area and foster collaboration amongst those working in software verification, formalised mathematics, and mathematical research, as well as help provide a shared understanding of the theory and tools for automated invention and discovery of mathematical theories.
