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)

Collection of Verification Tasks (MOVED, please follow the link)

Static analysis framework for C

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.

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)

Formalisation of the linear lambda calculus in Coq

DPLL(T)-based Verification tool for DNNs

Static & Dynamic Verification of C programs

Prototype functional programming language with refinement types, powered by Inox

LSVerifier - Large Systems Verifier

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

A consistency checker for probabilistic software quality models

A Model Checker in Rust