applications/science/logic

Tool for squential logic synthesis and formal verification

Interactive theorem prover

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

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

Extremely fast SMT solver for bit-vectors and arrays

Generic parser and tool package for the BTOR2 format

Simplified Satisfiability Solver

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

Interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Cur…

Linear logic programming system

Extension of clingo to handle constraints over integers

ASP system to ground and solve logic programs

ASP system to ground and solve logic programs

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

Coq proof assistant

Coq proof assistant

Coq proof assistant

Coq proof assistant

Advanced SAT Solver

Cryptographic protocol verifier in the computational model

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

Prover for satisfiability modulo theory (SMT)

High-performance theorem prover and SMT solver

High-performance theorem prover and SMT solver

Programming language with built-in specification constructs

Proof checker for unSAT proofs

Computer-Aided Cryptographic Proofs

Testing program for EasyCrypt formalizations

Fixpoint reasoning system that unifies Datalog and equality saturation

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

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

Automated first-order logic theorem prover

Java formal verification tool

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

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)

Automatic and interactive theorem prover

High-performance typed higher order prover

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

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

Draw SVG digital circuits schematics from yosys JSON netlists

New symbolic model checker for the analysis of synchronous finite-state and infinite-state systems

Symbolic model checker for analysis of finite and infinite state systems

High-performance theorem prover and SMT solver

Modal Homotopy Type System

Functional language for reasoning about formal systems

SAT solver binary based on the msat library

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

Satisfiability modulo theory (SMT) solver

Tool for the working semanticist

SAT solver with proof and core support

Program for proof-tree visualization

Automated theorem prover for first-order and equational logic

Cryptographic protocol verifier in the formal model

Proof assistant for Nominal Computational Type Theory

Automated theorem prover for higher-order logic

Tools for software verification and analysis

Fast solver for the #SAT model counting problem

Automated theorem prover for first-order logic

Verification of stateful processes (via Proverif)