Stars
An easy-to-learn/use static analysis framework for Java
Enumerative Testing and Bounded Validation of SMT Solvers
A blackbox mutational fuzzer for detecting critical bugs in SMT solvers
A powerful and user-friendly binary analysis platform!
A constraint-based program generator for testing program analyzers
The fuzzer afl++ is afl with community patches, qemu 5.1 upgrade, collision-free coverage, enhanced laf-intel & redqueen, AFLfast++ power schedules, MOpt mutators, unicorn_mode, and a lot more!
cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.
A miniature model of the Typescript compiler, intended to teach the structure of the real Typescript compiler
SMT Based Verification in Haskell. Express properties about Haskell programs and automatically prove them using SMT solvers.
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays and uninterpreted functions and their combinations. Its name …
CAV'22 paper to speed up Neural Network Verification.
Manage and switch between Solidity compiler versions
A TypeScript package providing a normalized typed Solidity AST along with the utilities necessary to generate the AST (from Solc) and traverse/manipulate it.
TypeScript types and a JSON Schema for the Solidity AST
SB Curated is a curated dataset of Solidity smart contracts annotated with tagged vulnerabilities. The dataset was created to evaluate the accuracy of automated analysis tools.
Sparkle is a Programming by Optimisation (PbO)-based problem-solving platform designed to enable the widespread and effective use of PbO techniques for improving the state-of-the-art in solving a b…