DreamGroup/MRG → ATX 2012

ATX 2012

IJCAR Workshop on Automated Theory eXploration
June 30 - July 1
Manchester, UK

Previous Workshops

Overview:

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.

Scope:

Theory exploration means the development of mathematical axioms, definitions, conjectures, theorems, examples and inference procedures as needed to cover the essential concepts and analysis tasks of mathematical and other application domains. The automation and mechanisation of these capabilities are much sought after in areas such as software verification, the analysis of computer systems, formalised mathematics and indeed mathematical research. The aim of the workshop is to bring together researchers with interests in any aspects of this area, including domain-specific formalisations, tool and theory development, and general-purpose frameworks for the structuring of theories and their maintenance.

Topics:

Theory exploration 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:

Programme:

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"

Submissions:

We invite submissions in 3 forms:

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.

Important Dates:

Program Committee:

Workshop Organisers:

On ATE and Automatheo:

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.

Important Dates

  • Submission (extended):
    3 April 2012
    17 April 2012
  • Notification (extended):
    8 May 2012
    18 May 2012
  • Final version (extended):
    5 June 2012
    10 June 2012
  • Workshop:
    30 June & 1 July, 2012