I am very excited to announce that the proposal by AdaCore and INRIA to work more closely inside a common research laboratory has been awarded a three-year funding from the French government, as part of the LabCom initiatiative of the ANR. We will work together between April and September to set up the common laboratory, which will officially start on October 1st of this year. I'm copying below the official summary describing our objectives with this common laboratory.
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 Toccata research team is 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.
AdaCore is an international SME, with a workforce shared between Europe 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. AdaCore has worked since 2008 with the Altran group around the SPARK proof technology.