The engineering of theories is essential to the exploitation of
mathematics in software engineering. We define a theory as a coherent
and consistent collection of definitions, axioms, theorems,
calculations and deduction rules, giving a reasonably complete
coverage of the essential concepts of some application area.
Such theories can be helpful in the design of systems, programs, APIs,
protocols, algorithms, design patterns, specification languages, and
programming languages. The principles of the theory should be
understandable by its users; but the detailed application of the
theory, and the checking of its correct use in particular cases,
should be assisted by automated tools and, wherever possible, hidden
from the users. To reconcile these interests is a significant
engineering task, and may require tools, which may perhaps be more
specialised than those which eventually mechanise the theory.
Tools that have assisted in theory engineering include interactive
theorem provers, automated theorem provers and SAT/SMT solvers such as
Coq, Specware, Hol, Z/Eves, B-tool, Prover9, SPASS, Vampire, STP,
Yices or Z3.
The purpose of this workshop is to bring together tool builders,
theory engineers and users to exchange experiences and ideas, and to
suggest how tools should be further developed to meet the needs of
theory engineering, and the wider application of theories developed on
other tools. Its ultimate goal is the creation of a Repository of
Challenges in the form of verification tasks and case studies to
stimulate this development.
