|Computer Laboratory >|
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.