[COLM 2024] A Survey on Deep Learning for Theorem Proving

The efficient SMT-based context-bounded model checker (ESBMC)

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 …

cvc5 is an open-source automatic theorem prover for Satisfiability Modulo Theories (SMT) problems.

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.

Bᴛᴏʀ2MLIR: A Format and Toolchain for Hardware Verification

Fast Symbolic Repair of Hardware Design Code

Sail RISC-V model

Automatic verification of LLVM optimizations

CirFix: Automatically Repairing Defects in Hardware Design Code

Experiments on automation for Lean

Lean 4 programming language and theorem prover

Tactics for discharging Lean goals into SMT solvers.

Verified graph rewriting (for dataflow circuits).

CLEVER: Code Lean Evaluation for Verified End-to-end Reasoning

ANSI-C benchmarks generated from Verilog RTL circuits with safety assertions. Used for Formal Property Verification.

The notes about programming language theory