Proving Alt-Ergo prover in Coq

I attended yesterday the PhD defense of Stéphane Lescuyer, who presented his work on the proof of prover Alt-Ergo, pushing the boundary of what’s feasible with today’s proof technology.

First, a few words of why this is interesting for us at AdaCore, in an industrial setting. Starting with SPARK Pro 9.1, users now have the possibility to call the prover Alt-Ergo to prove some formulas generated by the SPARK tool-set, in addition to the existing SPARK prover. Proving these formulas ensures that there are no run-time errors and that subprograms properly implement their contracts. Thus, it is crucial that the prover used is correct: whenever it says a formula is true, it must be the case. In project Hi-Lite (hosted on Open-DO), we also aim at using Alt-Ergo to prove functional properties of interest to a user on parts of an Ada codebase.

Second, the inner algorithms of such automatic provers are very tricky, so it is quite hard to show a convincing proof that they are correct. The well-known case is the Shostak’s method on which Alt-Ergo’s main algorithm is based: Shostak published his algorithm in 84, and despite many papers discussing the approach, the algorithm was erroneous on various accounts; it was corrected in two steps, in 1996 by Cyrluk, Lincoln and Shankar and in 2001 by Rueß and Shankar. Only a formal proof like the one done by Stéphane Lescuyer can then provide a strong argument for correctness.

Bottom line is that Alt-Ergo is built around a proven core, and that’s great news in order to use it in safety-critical software development and verification.

This entry was posted in Certification, Events and tagged , . Bookmark the permalink. Trackbacks are closed, but you can post a comment.

5 Comments

  1. comar
    Posted January 5, 2011 at 17:18 | Permalink

    how do you prove the correctness of the Coq proof?

  2. Yannick Moy
    Posted January 5, 2011 at 17:29 | Permalink

    Stéphane coded in Coq the core algorithm in Alt-Ergo, and proved that it was indeed producing the correct result by manual proof in Coq. The correctness of this proof then lies solely on the correctness of the Coq system, which is built so that only a very small core has to be trusted. No need to say, this very small core (a few hundred lines of code) has been thoroughly inspected by many, and is indeed trustable.

    • comar
      Posted January 6, 2011 at 14:57 | Permalink

      interesting… thanks for the details! Is there a “bootstrap” proof in Coq of the core of Coq itself? The other potential issue is the accuracy of the translation of the Alt-Ergo algorithms into Coq… but there is probably no simple solutions to that…

  3. Yannick Moy
    Posted January 6, 2011 at 20:08 | Permalink

    I don’t know about a ‘bootstrap’, which would not be foolproof anyway, so much efforts for few benefits. Instead, the Coq team has made the trusted core very small, so that they could be sure of its correctness by review.

    Regarding the match between prover Alt-Ergo (in OCaml) and the core Alt-Ergo implemented in Coq, this is a matter of making sure the published algorithm is properly implemented in each, which is also ensured by review.

  4. Johannes Kanig
    Posted January 10, 2011 at 18:28 | Permalink

    There has indeed been “Coq in Coq” proof, by Bruno Barras and Benjamin Werner. Similar to the work by Stéphane, it is not the implementation of Coq, but the theory of Coq that is proven. Also, for theoretical reasons, one can never prove the consistency of Coq inside Coq itself, so only a subset of the actual Coq system has been verified in that work. At least the introduction and conclusion of that paper make an interesting read.

Post a Comment

Your email is never published nor shared. Required fields are marked *

*
*
 
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org