PV4 Alt-Ergoproduces a satisfiability result for a formula

SMT solver

Application domain/field

SMT solving

Type of tool

SMT solver

Expected input

SMT formula


One of the following:

Expected output

Valid, Invalid or I don't know if the user used its native input language (.ae files). It can also output in the SMT-LIB 2 form if asked. unsat, sat or unknown if the user used the SMT-LIB 2 input format (i.e. .psmt2 or .smt2 files)


Alt-Ergo is used by Frama-C, SPARK, Why3, Atelier-B and Caveat.


Related papers

A Three-Tier Strategy for Reasoning About Floating-Point Numbers in SMT (CAV '17)

Last publication date

13 July 2017

ProVerB specific

Markdown description: view/edit

ProVerB is a part of SLEBoK. Last updated: February 2023.