categories

applications/science/logic

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
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