ATx'12/WInG'12: Editor's Preface

This volume contains the proceedings of the Workshop on Automated Theory Exploration (ATx). The workshop is the successor and merger of the International Workshop on Automated Theory Engineering (ATE) and the Workshop on Automated Mathematical Theory Exploration (Automatheo). It also contains the proceedings of the Workshop of Invariant Generation (WInG). Both workshops were both held in Manchester, UK, on June 2012 as satellite workshops of the 6th International Joint Conference on Automated Reasoning (IJCAR).

Automated 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.

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.

The diversity of topics relevant to theory exploration is reflected by the contributions to the workshop and to this volume. The workshop contained of 6 extended abstracts and 4 research papers; the latter are part of these proceedings. Each submission was refereed by three reviewers on its originality, technical soundness, quality of presentation and relevance to the workshop.

The ATx programme included one invited lecture by an expert in the area: "Proof Assistants and the Dynamic Nature of Formal Theories" by Robert L. Constable (Cornell University, USA).

Invariant Generation is a key ingredient in a broad spectrum of tools that help to improve program reliability and understanding: The ability to automatically extract and synthesise auxiliary properties of programs has had a profound effect on program analysis, testing, and verification over the last several decades. A key impediment for program verification is the overhead associated with providing, debugging, and verifying auxiliary invariant annotations. Releasing the software developer from this burden is crucial for ensuring the practical relevance of program verification. In the context of testing, suitable invariants have the potential of enabling high-coverage test-case generation. Especially promising breakthroughs are invariant generation techniques by Groebner bases, quantifier elimination, and algorithmic combinatorics, which can be used in conjunction with model checking, theorem proving, static analysis, and abstract interpretation.

WInG contained of 8 extended abstracts and 1 research paper associated with an invited tutorial; the latter is part of these proceedings. Each submission was refereed by at least three reviewers on its originality, technical soundness, quality of presentation and relevance to the workshop.

The WING programme also included one invited lecture by an expert in the area: "Specification Inference and Invariant Generation: A Machine Learning Perspective" Aditya V. Nori (Microsoft Research India).

We thank our colleagues without whose help and support the workshop would not have been possible. First, Birte Glimm, the satellite events chair and the local organisers for all their help. Second, the authors who supported this workshop by submitting papers and the invited speaker for their contributions. Third, the members of the Programme Committee for carefully reviewing and selecting the papers.