Alt-Ergo

Technologies

Design choices

Main components

Built-in theories

• empty theory
• linear integer arithmetic
• linear rational arithmetic
• non-linear arithmetic
• floating point arithmetic
• polymorphic arrays
• enumerated datatypes
• AC symbols
• record datatypes

  Industrial uses

• , a platform for deductive program verification, uses Alt-Ergo as its main prover;
• CAVEAT, a C-verifier developed by CEA and used by Airbus; Alt-Ergo was included in the qualification DO-178C of one of its aircraft;
• Frama-C, a framework to analyse C-code, uses Alt-Ergo in the Jessie and WP plugins ;
• SPARK, uses Alt-Ergo to automate the verification of some assertions in Spark 2014;
• Atelier-B can use Alt-Ergo instead of its main prover ;
• Rodin, a B-method framework developed by Systerel, can use Alt-Ergo as a back-end;
• , an open source model checker for verifying safety properties of array-based transition systems.
• , a toolset for reasoning about relational properties of probabilistic computations with adversarial code.