Static Analyzer and Verifier

BRICK: A Verifier for C code

C Bounded Model Checker

CPAchecker, the Configurable Software-Verification Platform (read-only mirror)

A verification tool for many memory models

DIVINE model checker git mirror, https://divine.fi.muni.cz. This is a read-only mirror of the main darcs repository. Issues should be reported using https://divine.fi.muni.cz/trac/report/1. Pull re…

A Hybrid Verification Tool for Finding Software Vulnerabilities in IoT Cryptographic Protocols

The efficient SMT-based context-bounded model checker (ESBMC)

Release snapshots of the Frama-C platform for source code analysis

An LLVM-based formal verification frontend for C programs.

Crucible is a library for symbolic simulation of imperative programs

Java Bounded Model Checker

SFI verifier of Wasm binaries