software-verification

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

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

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

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.

Map2Check: Finding Software Vulnerabilities

Read-only mirror of the Klever Git repository

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

Teaching and Learning Software Verification via SVF

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

Formalisation of the linear lambda calculus in Coq

Prototype functional programming language with refinement types, powered by Inox

Static & Dynamic Verification of C programs

A poly-language execution-based violation-witness validator

Rust software verification benchmarks

CakeML build tool

A consistency checker for probabilistic software quality models

Abstractly represent software error traces as finite automata.