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.

Publications

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

Containers for Specification in SPARK
Authors Claire Dross
Status Accepted at High Integrity Language Technologies, HILT 2022

The Work of Proof in SPARK
Authors Claire Dross
Status Accepted at Ada-Europe International Conference on Reliable Software Technologies, AEiC 2022

Making Proofs of Floating-Point Programs Accessible to Regular Developers
Authors Claire Dross and Johannes Kanig
Status Accepted at 1 13th Working Conference on Verified Software: Theories, Tools, and Experiments, VSTTE 2021

Dynamic Memory Management in Critical Embedded Software
Authors Cyrille Comar, Claire Dross, Florian Gilcher and Yannick Moy
Status Accepted at Embedded Real Time Systems, ERTS 2022

How the Analyzer can Help the User Help the Analyzer
Authors Yannick Moy
Status Accepted at 6th Workshop on Formal Integrated Development Environment, F-IDE 2021

Explaining Counterexamples with Giant-Step Assertion Checking
Authors Benedikt Becker, Cláudio Belo Lourenço and Claude Marché
Status Accepted at 6th Workshop on Formal Integrated Development Environment, F-IDE 2021

Verification of Programs with Pointers in SPARK
Authors Georges-Axel Jaloyan, Claire Dross, Maroua Maalej, Yannick Moy and Andrei Paskevich
Status Accepted at International Conference on Formal Methods and Software Engineering, ICFEM 2020

Recursive Data Structures in SPARK
Authors Claire Dross and Johannes Kanig
Status Accepted at Computer Aided Verification 2019

When Testing is Not Enough
Authors Yannick Moy and M. Anthony Aiello
Status Whitepaper

Practical Application of SPARK to OpenUxAS
Authors M. Anthony Aiello, Claire Dross, Patrick Rogers, Laura Humphrey, and James Hamil
Status Accepted at the International Symposium on Formal Methods, FM 2019, October 2019, Porto, Portugal

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