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)

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

An Exchange Format for Verification Witnesses

Read-only mirror of the Klever Git repository

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

Teaching and Learning Software Verification via SVF

Static & Dynamic Verification of C programs

CakeML build tool

Rust software verification benchmarks

A consistency checker for probabilistic software quality models

Abstractly represent software error traces as finite automata.

An interpreter for Denotational Semantics of While language

A Model Checker in Rust

Voila is proof outline checker for fine-grained concurrency verification

Formal Verification on NDN trust schema

Software Verification course project - Fixing bugs using a working example as a specification

(my verification project for cs5110 / cs6110) A vscode extension that adds live visualizations of alloy type structures to vscode. (also includes some basic some basic langauge support)

SafePKT Flavor of RVT (a collection of tools/libraries to support both static and dynamic verification of Rust programs.)

4th Year Honours Thesis on Programming Language Semantics

Language invariant AST abstraction with APIs to create, visualize or compare ASTs

Nidhugg is a bug-finding tool which targets bugs caused by concurrency and relaxed memory consistency in concurrent programs. It is particularly useful for programs written in C/pthreads. Currently Nidhugg supports the SC, TSO, PSO, POWER and ARM (partial) memory models.