Tag Archives: proof

Axioms and Proofs: When Less is More

In formal verification, we ultimately rely on automatic provers to decide whether formulas are valid (always true) or not. In GNATprove for example, we rely mostly on the ability of prover Alt-Ergo to analyze quickly the formulas we generate, and answer yes when the formula is valid or no when the formula is invalid (so [...]

Posted in Open Source | Also tagged , | Leave a comment

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 [...]

Posted in Certification, Events | Also tagged | 5 Comments
  • Categories

  • Open-DO Projects

  • Want to get involved?

  • Contact

    info @ open-do.org