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

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

Map2Check: Finding Software Vulnerabilities

Read-only mirror of the Klever Git repository

An Exchange Format for Verification Witnesses (MOVED, please follow the link)

Information to reproduce results from SV-COMP (MOVED, please follow the link)

DPLL(T)-based Verification tool for DNNs

LSVerifier - Large Systems Verifier

Formalisation of the linear lambda calculus in Coq

Static & Dynamic Verification of C programs

Prototype functional programming language with refinement types, powered by Inox

🌍 A poly-language execution-based violation-witness validator

A consistency checker for probabilistic software quality models