categories

Showing entries 1-100 out of 115.

A tool for squential logic synthesis and formal verification

Interactive theorem prover

A toolkit for developing ACG signatures and lexicon

And-Inverter Graph (AIG) utilities

SAT/PseudoBoolean/MaxSat/ASP solver using glucose

AIGER model checking for Property Directed Reachability

A SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted func…

An extremely fast SMT solver for bit-vectors and arrays

A generic parser and tool package for the BTOR2 format

Simplified Satisfiability Solver

CBMC is a Bounded Model Checker for C and C++ programs

An interactive theorem-prover and dependently typed programming language, based on extrinsic (aka …

Linear logic programming system

Extension of clingo to handle constraints over integers

ASP system to ground and solve logic programs

Resolution-based theorem prover for Coalition Logic implemented in C++

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

An advanced SAT Solver

Cryptographic protocol verifier in the computational model

An open source model checker for verifying safety properties of array-based systems

A prover for satisfiability modulo theory (SMT)

A high-performance theorem prover and SMT solver

A high-performance theorem prover and SMT solver

A proof checker for unSAT proofs

Computer-Aided Cryptographic Proofs

Testing program for EasyCrypt formalizations

Automated first-order theorem prover

Small tool to manage your installations of the Lean theorem prover

Automated theorem prover for full first-order logic with equality

Automated theorem prover for full first-order logic with equality

A domain-independent planning system

Formal Specifications for Verification and Synthesis

Verifying and formally proving properties on numerical programs dealing with floating-point or fix…

Modern, parallel SAT solver (sequential version)

Modern, parallel SAT solver (parallel version)

Interactive theorem prover based on Higher-Order Logic

Interactive theorem prover based on Higher-Order Logic

Interactive theorem prover based on Higher-Order Logic

An automated first-order logic theorem prover

A generic proof assistant

Java formal verification tool

A 'keep it simple and clean bare metal SAT solver' written in C

A symbolic virtual machine built on top of LLVM

Lambda calculus interpreter

Automatic and interactive theorem prover

Automatic and interactive theorem prover (version with HoTT support)

A high-performance typed higher order prover

An automated theorem prover for classical higher-order logic with choice

C library for manipulating polynomials

Fast SAT solver

Educational tool for designing and simulating digital logic circuits

Digital logic designer and simulator

Fast translation from LTL formulae to Buchi automata

A toolset for model-checking concurrent systems and protocols

Mutation-based coverage testing for hardware designs, with Yosys

Automatic theorem prover for first-order logic with equality

Compact and readable SAT solver

SMT solver for Monotonic Theories

Write formal proofs in natural language and LaTeX

Symbolic model checker for analysis of finite and infinite state systems

High-performance theorem prover and SMT solver

Modal Homotopy Type System

A functional language for reasoning about formal systems

State-of-the-art MaxSAT and Pseudo-Boolean solver

A satisfiability modulo theory (SMT) solver

A tool for the working semanticist

Safety and Liveness Analysis of Petri Nets with SMT solvers

SAT solver with proof and core support

A program for proof-tree visualization

Automated theorem prover for first-order and equational logic

Cryptographic protocol verifier in the formal model

A proof assistant for Nominal Computational Type Theory

Automated theorem prover for higher-order logic

Tools for software verification and analysis

Automated theorem prover for first-order logic

Verification of stateful processes (via Proverif)

Simple Theorem Prover

Tooling for Yosys-based verification flows

A (concrete or symbolic) implementation of IEEE-754 / SMT-LIB floating-point

Security protocol verification in the symbolic model

IDE for the TLA+ tools

An algorithm specification language with model checking tools

Mechanically check TLA+ proofs

Thousands of problems for theorem provers and tools