Slides from the Event now available
Click the titles to expand each session and find a link to view the slides for each presentation.
- 10:15 - 10:45 Welcome
10:45 - 11:00 Scientific and Technical Objectives of ProofInUse
Claude Marché, Director of 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.
11:00 - 11:30 Deductive Program Verification with Why3, Past and Future
Claude Marché, Inria
We present an overview of the Why3 environment for deductive program verification. It provides a rich language for formal specification and programming, allowing one to develop algorithms and programs, and prove them sound. Why3 comes with a rich standard library of both logical theories for specifications and data structures for programming. Why3 relies on external theorem provers, both automated and interactive, to discharge verification conditions. During the past years, Why3 has been used as an intermediate language the verification of Java, C and now Ada programs.
Claude Marché is the team leader of Toccata Inria research team, and director of the ProofInUse joint laboratory. His research focuses on techniques for automatic deduction and specification languages, in particular applied to formal program verification. This research is supported by the implementation of practical tools for formal program verification in C (Caduceus, Jessie plugin of Frama-C) and Java (Krakatoa), all based on the Why3 platform. Claude has been advising 12 PhDs on these subjects, and publishing the results in many journals and conferences.
11:30 - 12:00 Formal Program Verification For All with SPARK 2014
Yannick Moy, AdaCore
SPARK is a programming language targeted at safety- and security-critical applications. The latest version, SPARK 2014, builds on the new specification features added in Ada 2012. As a result, formal specifications can be tested and debugged like code, which goes a long way to making them accessible to all programmers. Three other features of the new toolset contribute to this democratization of formal verification: the level of proof automation, practical user interaction and the integration in existing processes based on testing. In this talk, we will present the challenges we face to further improve the SPARK technology, based on the rapidly evolving capabilities offered by SMT solvers.
Yannick Moy is a Senior Software Engineer at AdaCore and co-director of the ProofInUse joint laboratory. At AdaCore, he works on software source code analyzers CodePeer and SPARK, aiming either at detecting bugs or at verifying safety/security properties. Yannick leads the developments of SPARK 2014, a product he presents in articles, conferences, classes and blogs (in particular www.spark-2014.org). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.
- 12:00 - 13:30 Lunch Break (buffet)
13:30 - 14:15 Alt-Ergo: An SMT Solver for Software Verification
Mohamed Iguernelala, OCamlPro
In this talk, we will present Alt-Ergo, an SMT solver tuned for proof obligations generated by program verification frameworks. We will focus in particular on its general architecture, its input language and its capabilities. Performances are illustrated on a set of benchmarks coming from program verification tools. Finally, we discuss a list of features and improvements we would like to further investigate.
Mohamed Iguernelala is a senior "Research and Development" engineer at OCamlPro SAS and a "Research Associate" in the VALS team of "Laboratoire de Recherche en Informatique" (LRI, UMR 8623). He received a PhD in Computer Science from Paris-Sud University. During his thesis, he worked on the enhancement of the Alt-Ergo SMT solver: an automatic theorem prover for first-order formulas. His research activities focus on automated reasoning, decision procedures and their combination in the "Satisfiability Modulo Theories" framework.
14:15 - 15:00 The CVC4 SMT Solver
Morgan Deters, New York University (presented by Martin Brain)
Satisfiability Modulo Theories (SMT) solvers leverage research advances in SAT solving and decision procedures to solve Boolean combinations of constraints written in an expressive language combining different background theories. CVC4 is a solver for these SMT problems with a number of features useful in verification, static analysis, synthesis, symbolic execution, and other domains. This talk includes an overview of SMT and describes the main features of CVC4. I will discuss various aspects of CVC4's internals, including its architecture, its capacity for dealing with quantifiers, its proof support, and its bitvector solver. CVC4, jointly developed at New York University and the University of Iowa, is freely available for both research and commercial use under an open-source license.
Morgan Deters is a senior research scientist at New York University's Courant Institute of Mathematical Sciences. His chief research interests include the construction of SAT- and SMT-solving tools, compiler support for advanced programming constructs, and software verification. He has been involved in SAT and SMT research for years, and has been involved in the design and development of CVC4 since its inception. Dr. Deters earned his Ph.D. in computer science at Washington University in St. Louis in 2007.
Morgan unexpectedly passed away on January 17th. Martin Brain, also a developer of CVC4, kindly accepted to replace Morgan for this presentation.
15:00 - 15:45 Popop: SMT Meets CP
François Bobot, CEA
The field of automatic reasoning evolved in many different directions, from the development of very powerful higher-order logics aiming at the mechanization of mathematics, to the design of efficient decision procedures tailored to propositional logic (SAT DPLL). Between these two extremes, SMT and CP are interested in efficient decision procedures for particular first-order theories with more or less restricted forms of quantification. The SMT and CP communities went there own way thirty years ago. In this presentation we will outline the difference between the SMT and CP current architecture and show how the generalization of boolean CDCL into the MC-SAT framework gives an opportunity to combine the SMT and CP communities. The last part of the talk will sketch the architecture of a prover that combine these techniques.
François Bobot is currently a Research Engineer at CEA in the Software Reliability Lab (LSL) where he is involved in the Weakest-Precondition Plugin in the Frama-C Plateform and in automatic solvers as PI of the ANR SOPRANO. He also participates in the development of other projects as Why3, CVC4 and OCaml.
15:45 - 16:30 Bit-Exact Automated Reasoning about Floating-Point Using SMT Solvers
Martin Brain, University of Oxford
The majority of new instrumentation and control systems, even those that are safety critical, make use of floating-point numbers. Thus the value of computed generated assurance evidence (including verification, test coverage, etc.) depends on the correctness, completeness and efficiency of automated reasoning about floating-point expressions. In this talk we will review the SMT-LIB Theory of Floating-Point, its semantics and the rationale behind key design decisions as well as surveying the current state-of-the-art in solver technology and future research directions. We aim to provide system integrators with sufficient information to integrate floating-point support into SMT interfaces and solver developer enough ideas to work on the next generation of floating-point reasoning.
Martin Brain is a post-doc researcher in the automatic verification group of the Department of Computer Science, University of Oxford. As part of the CProver team, he focuses on using automatic theorem provers (such as SAT and SMT solvers) to analyse C and other low level software to generate test cases, find bugs and prove safety. Particular areas of expertise include numerical and floating-point programs (for control or data processing), the use of abstractions in reasoning and supporting industrial users in integrating verification research into their tools and services. He is a co-author of the Riposte counter-example generation tool for SPARK.
- 16:30 - 17:00 Break
17:00 - 17:15 Présentation générale du labo commun ProofInUse et de ses objectifs (en français / in French)
Claude Marché, Inria
Nous décrirons l'intérêt qu'ont AdaCore et Inria à collaborer au sein du laboratoire commun ProofInUse, et nous ferons une présentation synthétique des objectifs du laboratoire pour les deux années et demi à venir.
- 17:15 - 17:45 Séance de questions / réponses avec le Comité Exécutif et le Comité Scientifique et Stratégique (en français / in French)
Sandrine Blazy, Professor at University of Rennes
Nozha Boujemaa, Director of Inria-Saclay Research Center
Cyrille Comar, President of AdaCore
Florent Kirchner, Director of CEA Software Safety Lab
Emmanuel Ledinot, Head of Scientific Studies, Dassault Aviation
David Lesens, Software Expert, Airbus Defence & Space
Claude Marché, Senior Scientist, Inria
Yannick Moy, Senior Software Engineer, AdaCore
- 17:45 Cocktail
Novotel Paris Gare Montparnasse
17 rue du Cotentin
75015 PARIS FRANCE
Registration is free but mandatory for attending the event.