Published: 30th July 2015 DOI: 10.4204/EPTCS.186 ISSN: 2075-2180 |
Preface | |
Invited Presentation: Reflection, of all shapes and sizes Georges Gonthier | 1 |
Invited Presentation: The VeriFast program verifier and its SMT solver interaction Bart Jacobs | 2 |
Importing SMT and Connection proofs as expansion trees Giselle Reis | 3 |
A framework for proof certificates in finite state exploration Quentin Heath and Dale Miller | 11 |
Systematic Verification of the Modal Logic Cube in Isabelle/HOL Christoph Benzmüller, Maximilian Claus and Nik Sultana | 27 |
The Common HOL Platform Mark Adams | 42 |
Checking Zenon Modulo Proofs in Dedukti Raphaël Cauderlier and Pierre Halmagrand | 57 |
Translating HOL to Dedukti Ali Assaf and Guillaume Burel | 74 |
Mixing HOL and Coq in Dedukti (Extended Abstract) Ali Assaf and Raphaël Cauderlier | 89 |
This volume of EPTCS contains the proceedings of the Fourth Workshop on Proof Exchange for Theorem Proving (PxTP 2015), held on August 2-3, 2015 as part of the International Conference on Automated Deduction (CADE 2015) in Berlin. The PxTP workshop series brings together researchers working on various aspects of communication, integration, and cooperation between reasoning systems and formalisms.
The progress in computer-aided reasoning, both automated and interactive, during the past decades, made it possible to build deduction tools that are increasingly more applicable to a wider range of problems and are able to tackle larger problems progressively faster. In recent years, cooperation of such tools in larger verification environments has demonstrated the potential to reduce the amount of manual intervention. Examples include the Sledgehammer tool providing an interface between Isabelle and (untrusted) automated provers, and also collaboration of the HOL Light and Isabelle systems in the formal proof of the Kepler conjecture.
Cooperation between reasoning systems relies on availability of theoretical formalisms and practical tools to exchange problems, proofs, and models. The PxTP workshop strives to encourage such cooperation by inviting contributions on suitable integration, translation and communication methods, standards, protocols, and programming interfaces. The workshop welcomes the interested developers of automated and interactive theorem proving tools, developers of combined systems, developers and users of translation tools and interfaces, and producers of standards and protocols. We are interested both in success stories and in descriptions of the current bottlenecks and proposals for improvement.
Previous editions of the workshop took place in Wrocław (2011), Manchester (2012), and Lake Placid (2013).
The workshop features seven regular papers and two invited talks by Georges Gonthier (Microsoft Research) and Bart Jacobs (University of Leuven).
We would like to thank the authors for submitting papers of high quality to these proceedings, the programme committee and external reviewers for diligently reviewing the submissions, and the organisers of CADE 2015 for their help in organizing PxTP 2015.
July 6, 2015
Cezary Kaliszyk
Andrei Paskevich
Although it is only a technical term for the common operation of quotation, reflection has had an increasingly important role in the design, organisation, and interconnection of machine formalizations of large theories. Reflexion supports a straightforward method for porting statements, deductions or proof techniques between theories, systems, or even logics: quote in one context to pure text, then reinterpret in a new context. While traditional logicians and computer programmers both have mostly focused on generic quoters and interpreters, computer proofs rely on a wider variety of reflexion forms. In a formal proof the interpretation must carry over meaning across contexts (the interpreter must be provably correct), and this is often easier with a shallower embedding in which not everything is quoted.
Reflection can be used at many scales: from the large scale in which complete problems are shipped to be solved in a different system, to the very small scale that mostly mediates between the flexibility of traditional notation and the rigorous regularity of formal representations, through a medium scale where the interpreter performs significant computation and produces readable notation.
This range of uses is supported by a range of implementation techniques. Quotation can be external (tactics, static overloading), or internal (first- or higher-order unification); interpretation can be deep, shallow, or even parallel. Together these techniques provide a toolkit that makes reflection far easier to use effectively. They have been instrumental in my work on the Four Colour and Odd Order theorems, from which this talk will draw several worked examples.
VeriFast is a tool that takes as input a set of C or Java source code files, annotated with specifications and logical definitions written in a variant of separation logic, and then, without further user interaction and usually in a matter of seconds, reports either "0 errors found" or a failed symbolic execution trace. In the former case, barring tool bugs, the program does not access unallocated memory, perform data races, or violate API or library preconditions or the user-provided specifications. The tool operates by symbolically executing each function/method, starting from a symbolic state representing an arbitrary state that satisfies the precondition, and checking that the final state satisfies the postcondition. The symbolic state consists of a symbolic store (mapping local variables to terms of first-order logic), a symbolic heap (a list of so-called chunks, interpreted as a separating conjunction of separation logic predicate applications, whose arguments are terms of first-order logic), and the path condition (a formula of first-order logic). Heap effects are dealt with in the tool itself through simple pattern matching, but proof obligations about data values are delegated to an SMT solver. We have taken care to keep hypotheses pushed into the SMT solver light on quantifiers and disjunctions. The axiomatization of inductive datatypes and primitive recursive functions prevents case splitting and (almost) prevents matching loops. Since neither the tool nor the SMT solver perform significant search, performance is predictable and good. VeriFast supports both Z3 and our own Redux (a partial re-implementation of Simplify).
I will first give an introduction to the specification and proof constructs in VeriFast's input language, then talk about how in VeriFast work is split between the front-end symbolic execution and the back-end SMT solver, going into detail on the encoding strategy, and then give a demo of the kind of user experience this produces.