ElNiak / awesome-formal-verification
Welcome to the ultimate list of resources for formal verification techniques and tools. This repository aims to provide an organized collection of high-quality resources to help professionals, researchers, and enthusiasts stay updated and advance their knowledge in the field.
☆25Updated 3 months ago
Alternatives and similar repositories for awesome-formal-verification:
Users that are interested in awesome-formal-verification are comparing it to the libraries listed below
- Binary analysis in HOL☆37Updated last month
- Schedule for ArtOfSAT☆10Updated last year
- A model-based API Fuzzer for SMT Solvers.☆14Updated 2 weeks ago
- Interactive Theorem Proving course using HOL4☆11Updated last year
- A Flexible and Efficient Proof Checker for SMT Solvers☆23Updated last week
- Tutorials and courses for Z3☆76Updated last week
- An curated list of papers on program synthesis.☆69Updated 5 years ago
- Clade is a tool for extracting information about software build process and source code☆21Updated last year
- Pono: A flexible and extensible SMT-based model checker☆99Updated this week
- gradient-based symbolic execution engine implemented from scratch☆35Updated last year
- A precise and scalable pointer analysis for LLVM, written in Ascent☆66Updated last month
- CBMC Viewer scans the output of CBMC and produces a browsable summary of its findings, making it easy to root cause the issues it finds.☆32Updated last month
- A Python model checking package☆65Updated 7 months ago
- DIVINE model checker git mirror, https://divine.fi.muni.cz. This is a read-only mirror of the main darcs repository. Issues should be rep…☆21Updated 4 years ago
- A Low Barrier Proof Assistant☆108Updated 2 weeks ago
- The Ultimate program analysis framework.☆217Updated this week
- MachSMT: An ML-Driven Algorithm Selection tool for SMT Solvers☆23Updated 2 years ago
- Public-facing course info for program analysis materials.☆41Updated 4 months ago
- Translate Python code to Coq code for formal verification. Applied to the reference implementation of Ethereum in Python.☆33Updated 7 months ago
- ☆26Updated last week
- Program Analysis, Software Verification & Testing. Python3, CAS, Dafny, Z3, CVC4, UCLID, ZChaff, NuSMV, AFL, Scala, CBMC & LLVM Framework…☆37Updated 2 years ago
- CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.☆18Updated 3 years ago
- VSCode extension that is designed to help automate writing of Coq proofs.☆100Updated 2 weeks ago
- The axiom profiler for exploring and visualizing SMT solver quantifier instantiations (made via E-matching).☆32Updated 2 months ago
- Information about verification tools. Browse the data at https://slebok.github.io/proverb/☆26Updated last year
- Bonn Lean course for winter 24/25☆29Updated 4 months ago
- Genetic program repair using GHC☆30Updated 11 months ago
- ComPy-Learn is a framework for exploring program representations for ML4CODE tasks.☆23Updated last year
- Automatically generate a compiler using equality saturation☆28Updated last year
- Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, floating-point arithmetic, arrays a…☆247Updated last week