Friday 05 February 2016, 10:30, LSV: Automated Deduction and Proof Certification for the B Method Set Theory, Pierre HALMAGRAND (Cnam / Inria).

The B method is a formal method used to specify and develop safety critical software in the railway industry, and which relies on an ad-hoc set theory extended with a particular typing system. To ensure the soundness of a B project, users have to verify large amounts of proof obligations (POs) during the development process.

The main goal of our work is to improve the automated verification of B method POs, and to increase confidence by using external proof checker to certify proofs. We propose a new tool, called Zenon Modulo, an extension of the tableau-based automated theorem prover (ATP) Zenon. We focus in this presentation on two important extensions. An extension to a ML-typed proof search, allowing us to deal with theories using ML-style polymorphism. And an extension to deduction modulo, a formalism that improves proof search in axiomatic theories by turning axioms into rewrite rules.

One important feature of Zenon Modulo is its ability to generate proof certificates for a proof checker called Dedukti, a logical framework that implements the lambda-Pi calculus modulo. Finally, we present some experimental results, based on a benchmark provided by industrial partners, and we compare Zenon Modulo to other state-of-the-art ATPs.