Binary Analysis Platform

Symbiotic is a tool for finding bugs in computer programs based on instrumentation, program slicing and KLEE

2022 年春季学期清华大学《软件分析与验证》课程实验平台

Code2Inv: Learning Loop Invariants for Program Verification

Generates loop invariants for program verification

📚 a modular easy to use Library for Static Analysis aiming at multi-language analysis

DIG is a a dynamic invariant generation tool that infers program invariants or properties over (i) program execution traces or (ii) program source code (C, Java, Java bytecode). DIG supports many forms of numerical invariants, including nonlinear equalities, octagonal and interval properties, min/max-plus relations, and congruence relations. DIG…

Template project for program verification in Coq, showcasing reasoning on CompCert's Clight language using the Verified Software Toolchain [maintainer=@palmskog]

SHAPE/S∀F∃: static prover/type-checker for N-D array programming in Scala, a use case of intuitionistic type theory

BAP python bindings

LLOV: LLVM OpenMP Verifier - : A Fast Static Data-Race Checker for OpenMP Programs

Information about verification tools. Browse the data at https://slebok.github.io/proverb/

This repository is intended for the Functional Programming and Verification (EIDI2) revision courses 2016 and 2017 at the Technical University of Munich.

An OpenAI gym environment for automated rule-based deductive program verification in KeY.

Rust frontend for LiSA

Strong non-interference for fine-grained concurrent programs

GCL verification tool based on predicate transformers

TACAS'23: Verification-guided Programmatic Controller Synthesis

DataRaceBench 1.2 kernels written in FORTRAN for LLVM-IR based data race detection tools

Voila is proof outline checker for fine-grained concurrency verification