Proofinuse

The objective of the joint laboratory ProofInUse is to provide verification tools, based on mathematical proof, to industry users. These tools would be aimed at replacing or complementing the existing test activities, whilst reducing costs.

ProofInUse originates from the sharing of resources and knowledge between the Toccata research team, specializing in techniques for program proofs and the SME AdaCore, a software publisher, specializing in providing software development tools for critical systems. A previous successful collaboration between Toccata and AdaCore enabled Toccata’s Why3 technology, to be put into the heart of the AdaCore-developed SPARK technology.

The purpose of the joint laboratory ProofInUse is to increase significantly the number of industrial customers of the SPARK technology, thus democratizing the use of proof techniques. This democratization requires the resolution of several scientific and technological challenges:

A first axis of research and innovation is to facilitate the use of automatic provers.

This first aspect requires the provision of a better interaction with the user, especially for debugging non-provable specifications as it is customary to expect for other development activities. Then, the joint laboratory will aim at improving the ratio of provability of programs commonly used in industry, in particular for numerical computations and data manipulations. Indeed, the economic interest of proof techniques is based largely on their automation, hence any improvement in this respect will result in the SPARK technology becoming more attractive. These two points require scientific breakthroughs in terms of support to the generation of counter-examples and modeling of data types adapted to the intrinsic capacities of automated provers.

A second axis of research and innovation is to allow the user to go beyond what is possible with the current SPARK technology, in terms of specification of programs and the proofs of these specifications.

On the specification side, it will require the support for more complex constructions in the Why3 technology, permitting the extension of the programming language included in SPARK. This will, in particular, satisfy the user’s need to specify data invariants. On the proof side, the objective of the joint laboratory is to give the user the possibility to guide the proof for more complex properties - for instance, those resistant to automated provers. These two points require scientific advances not only at the level of the intermediate language constructs used for proofs, but also in the methods for generating proof obligations, permitting these uses.

The Team

Proof Team Claude

Claude Marché Director
Inria
Research Director, leader of the Toccata research team.

Proof Team Yannick

Yannick Moy co-director
AdaCore
Software engineer, product manager of the SPARK technology.

Proof Team Claire

Claire Dross
AdaCore
Software engineer, leading developer of the SPARK technology.

Proof Team Jc

Jean-Christophe Filliâtre
CNRS
Researcher, main developer of the Why3 technology.

Proof Team Johannes

Johannes Kanig
AdaCore
Software engineer, technical leader of the SPARK technology.

Proof Team Andrei

Andrei Paskevich
Université Paris-Sud 11
Teaching assistant, second main developer of the Why3 technology.

Dailler

Sylvain Dailler
Inria
Research Engineer

Proof Team Maalej

Maroua Maalej
AdaCore
Postdoctoral Researcher

Previous Members

Clement Fumex

Clément Fumex
Inria
Research Engineer

Hauzar

David Hauzar
Inria
Research Engineer

About the Toccata research team

Part of INRIA Saclay and the Laboratoire de Recherche en Informatique (UMR Université Paris-Sud and CNRS). This team develops and distributes software for program proof. The Toccata team collaborated for nearly ten years with industry users of these tools, including Airbus, Dassault-Aviation, Gemalto.

About AdaCore

AdaCore is an international software engineering company based in France and the United States. AdaCore develops and distributes software for the development of critical systems, in particular the GNAT Pro development environment for the Ada programming language. As part of a long-term partnershuip, AdaCore has worked since 2008 with the Altran group on the SPARK proof technology.

Publications

A gallery of examples in Why3 and SPARK developed as part of ProofInUse activities is available on the website of Toccata Inria team.

Instrumenting a Weakest Precondition Calculus for Counterexample Generation
Authors Sylvain Dailler, David Hauzar, Claude Marché and Yannick Moy
Status Published in the Journal of Logical and Algebraic Methods in Programming

Borrowing Safe Pointers from Rust in SPARK
Authors Georges-Axel Jaloyan, Yannick Moy and Andrei Paskevich
Status Draft

Climbing the Software Assurance Ladder - Practical Formal Verification for Reliable Software
Authors Claire Dross, Guillaume Foliard, Théo Jouanny, Lionel Matias, Stuart Matthews, Jean-Marc Mota, Yannick Moy, Pascal Pignard and Romain Soulat
Status Accepted at the 18TH International Workshop on Automated Verification of Critical Systems, July 2018, Oxford, UK

Lightweight Interactive Proving inside an Automatic Program Verifier
Authors Sylvain Dailler, Claude Marché and Yannick Moy
Status Accepted at the 4th Workshop on Formal Integrated Development Environment, July 2018, Oxford, UK

Safe Dynamic Memory Management in Ada and SPARK
Authors Maroua Maalej, Yannick Moy and Tucker Taft.
Status Accepted at the 23rd International Conference on Reliable Software Technologies, Ada-Europe 2018, June 2018

A formally proved, complete algorithm for path resolution with symbolic links
Authors 
Ran Chen, Martin Clochard, and Claude Marché.
Status Published in the Journal of Formalized Reasoning, December 2017

A Three-tier Strategy for Reasoning about Floating-Point Numbers in SMT
Authors Sylvain Conchon, Mohamed Iguernlala, Kailiang Ji, Guillaume Melquiond and Clément Fumex
Status Accepted at the 29th International Conference on Computer Aided Verification, July 2017, Heidelberg, Germany

Automating the Verification of Floating-Point Programs
Authors Clément Fumex, Claude Marché and Yannick Moy
Status Accepted at the 9th Working Conference on Verified Software: Theories, Tools and Experiments, July 2017, Heidelberg, Germany

Automated Verification of Floating-Point Computations in Ada Programs
Authors Clément Fumex, Claude Marché and Yannick Moy
Status Research Report RR-9060, Inria Saclay Ile-de-France, April 2017

Auto-Active Proof of Red-Black Trees in SPARK
Authors Claire Dross and Yannick Moy
Status Accepted at NASA Formal Methods, June 2017, Moffett Field, California, United States

A formal proof of a Unix path resolution algorith
Authors Ran Chen, Martin Clochard, and Claude Marché
Status Research Report RR-8987, Inria Saclay Ile-de-France, December 2016

Static versus Dynamic Verification in Why3, Frama-C and SPARK 201
Authors Nikolai Kosmatov, Claude Marché, Yannick Moy, and Julien Signoles
Status Accepted at 7th International Symposium on Leveraging Applications of Formal Methods, Verification and Validation, Oct 2016, Corfu, Greece

Counterexamples from Proof Failures in SPARK
Authors David Hauzar, Claude Marché, and Yannick Moy
Status Accepted at Software Engineering and Formal Methods, July 2016, Vienna, Austria

Specification and Proof of High-Level Functional Properties of Bit-Level Programs
Authors Clément Fumex, Claire Dross, Jens Gerlach, and Claude Marché
Status Accepted at NASA Formal Methods, June 2016, Minneapolis, United States

Abstract Software Specifications and Automatic Proof of Refinement
Authors Claire Dross and Yannick Moy
Status Accepted at the 1st International Conference on Reliability, Safety and Security of Railway Systems (RSSR 2016), June 2016

Counterexamples from proof failures in the SPARK program verifier
Authors David Hauzar, Claude Marché, and Yannick Moy
Status Research Report 8854, Inria, February 2016

High-level functional properties of bit-level programs: Formal specifications and automated proofs
Authors Claire Dross, Clément Fumex, Jens Gerlach, and Claude Marché
Status Research Report 8821, Inria, December 2015

Adding Decision Procedures to SMT Solvers using Axioms with Triggers
Authors Claire Dross, Sylvain Conchon, Johannes Kanig, Andrei Paskevich
Status Published in the International Journal of Automated Reasoning, November 2015

How to avoid proving the absence of integer overflows
Authors Martin Clochard, Jean-Christophe Filliâtre, and Andrei Paskevich
Status In Arie Gurfinkel and Sanjit A. Seshia, editors, 7th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Lecture Notes in Computer Science, San Francisco, California, USA, July 2015. Springer

Bridging the gap between testing and formal verification in Ada development
Authors Claude Marché and Johannes Kanig
Status ERCIM News, 100:38--39, January 2015

Explicit Assumptions - A Prenup for Marrying Static and Dynamic Program Verification
Authors Johannes Kanig, Rod Chapman, Cyrille Comar, Jérôme Guitton, Yannick Moy and Emyr Rees
Status Accepted at the 8th International Conference on Tests & Proofs

Formalizing Semantics with an Automatic Program Verifier
Authors Martin Clochard, Jean-Christophe Filliâtre, Claude Marché and Andrei Paskevich
Status Accepted at the 6th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), volume 8471 of Lecture Notes in Computer Science, pages 37-51, Vienna, Austria, July 2014. Springer

[OUTSIDE PROOFINUSE] A Proof Infrastructure for Binary Programs
Authors Ashlie B. Hocking, Benjamin D. Rodes, John C. Knight, Jack W. Davidson and Clark L. Coleman
Status Accepted at NASA Formal Methods, Jun 2016, Minneapolis, United States

[OUTSIDE PROOFINUSE] Progress-Sensitive Security for SPARK
Authors Willard Rafnsson, Deepak Garg and Andrei Sabelfeld
Status Accepted at the International Symposium on Engineering Secure Software and Systems, April 2016, London, UK

Sponsors

adacore.png#asset:42461

anr.png#asset:42466

altran.png#asset:42468

cnrs.png#asset:42469

inria.png#asset:42470

universite-paris-sud.png#asset:42471