A static code analyser for C/C++ (up to C++17, mixed C/C++ codebases) that proves the absence of runtime errors and invalid concurrent behaviour.
- Covers undefined behaviour, uncaught runtime errors, and hardware specifics.
-
Sound No errors signalled
$\Rightarrow$ proved absence of errors.
Satisfies the National Institute of Standards and Technology (NIST) criteria for sound static code analysis.
Used for industrial safety-critical applications, including by Airbus, ESA & Bosch.
A [[Symbolic Execution]] engine that can be used for some verification, and automatic unit test generation.
A bounded [[Model Checker]] for C/C++ (C89,99 & C++11). It is also used by Kani (a CBMC frontend for verifying rust code).
A modular C verifier.
Used by meta for bug-finding within their large codebase.
A model checker using its own language-agnostic intermediate representation.
- Supports verification based on [[Separation Logic Without Functions]]
- Supports both Javascript and C, exploring a Rust frontend [[Gillian]]
A framework for reasoning about concurrent programs using [[Coq]]