Formal Software Verification
- Coq – Coq is a formal proof management system. It provides a formal language to write mathematical definitions, executable algorithms and theorems together with an environment for semi-interactive development of machine-checked proofs.
- Why3 – Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions.
- Alt-Ergo – Alt-Ergo is an open-source SMT solver dedicated to the proof of mathematical formulas generated in the context of program verification.
- Imandra - Imandra is a cloud-native automated reasoning engine for ReasonML/OCaml supporting formal verification and symbolic reasoning. Imandra has many advanced features, including first-class computable counterexamples, symbolic model checking, support for polymorphic higher-order recursive functions, automated induction, a powerful simplifier and symbolic execution engine with lemma-based conditional rewriting and forward-chaining, first-class state-space decompositions, decision procedures for algebraic datatypes, floating point arithmetic, and much more.
- VOLPIC - VOLPIC is a pipeline for lifting and verifying Pascal code in Coq. It provides a transpiler to convert Pascal source code into Coq source code, theorem and notation libraries for verifying lifted code, and an extraction libary to extract the verified algorithms into OCaml source code.