A static analyzer for Java, C, C++, and Objective-C

Binary Analysis Platform

A lightweight, modular standard library extension, string library, and interfaces to various libraries (unix, threads, etc.) BSD license.

BINSEC binary-level open-source platform

The Zarith library implements arithmetic and logical operations over arbitrary-precision integers and rational numbers. The implementation, based on GMP, is very efficient.

Static analysis framework for C

Infrastructure for Reassembleable Disassembling and Transformation

The formal proof of the Kepler conjecture

An automatic theorem prover in OCaml for typed higher-order logic with equality and datatypes, based on superposition+rewriting; and Logtk, a supporting library for manipulating terms, formulas, cl…

OCamlPro public development repository for Alt-Ergo

The Sparrow Static Analyzer

Shoo is a statically typed programming language with first-class functions, structs, and arrays.

Algebraic, staged parsing for OCaml: typed, compositional, and faster than yacc

a safety verifier for Solidity smart contracts

An automated deductive program verifier.

十分钟魔法练习 in OCaml

Constraint solver based on abstract domains

Duet: static analysis for unbounded concurrency

A proof-producing SMT/McSat solver, handling polymorphic first-order logic, and using an SMT/McSat core extended using Tableaux, Superposition and Rewriting.

Experimental model finder/SMT solver for functional programming.

Bidirectional transformation for Relational view update Datalog-based Strategies

DAI: Demanded Abstract Interpretation

QUICr parametric abstract domain for sets

Invariant generator for polynomial loops

Symbolic Reasoning Kit

[wip] functorial library with classic algorithms for arithmetic

Preprocessors and analyzers for SMT-LIB