Static analyzer for C/C++ based on the theory of Abstract Interpretation.
Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE
Static Analyzer for LLVM bitcode based on Abstract Interpretation. **Update**: clam is still actively maintained. Please use branch dev14.
CPAchecker, the Configurable Software-Verification Platform (read-only mirror)
Static analysis framework for C
Collection of Verification Tasks (MOVED, please follow the link)
Curated List of Research Focused Reading Materials & Videos for Learning about Programming Language Theory Research, Formal Methods and their application in some most active computer Science fields.
The CBMC starter kit makes it easy to add CBMC verification to a software project.
Teaching and Learning Software Verification via SVF
Read-only mirror of the Klever Git repository
An Exchange Format for Verification Witnesses (MOVED, please follow the link)
DPLL(T)-based Verification tool for DNNs
Information to reproduce results from SV-COMP (MOVED, please follow the link)
LSVerifier - Large Systems Verifier
Formalisation of the linear lambda calculus in Coq
Prototype functional programming language with refinement types, powered by Inox
The ESBMC ibmc (Invariant Based Model Checking) Tool.
🌍 A poly-language execution-based violation-witness validator