Showing entries 1-100 out of 130.
isabelleapplications/science/logic/isabelle
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
clingoclasp
ASP system to ground and solve logic programs
clingoclingo
ASP system to ground and solve logic programs
clingogringo
ASP system to ground and solve logic programs
Resolution-based theorem prover for Coalition Logic implemented in C++
coqcoq
Coq proof assistant
coqcoq_8_10
Coq proof assistant
coqcoq_8_11
Coq proof assistant
coqcoq_8_12
Coq proof assistant
coqcoq_8_13
Coq proof assistant
coqcoq_8_14
Coq proof assistant
coqcoq_8_15
Coq proof assistant
coqcoq_8_16
Coq proof assistant
coqcoq_8_17
Coq proof assistant
coqcoq_8_18
Coq proof assistant
coqcoq_8_19
Coq proof assistant
coqcoq_8_5
Coq proof assistant
coqcoq_8_6
Coq proof assistant
coqcoq_8_7
Coq proof assistant
coqcoq_8_8
Coq proof assistant
coqcoq_8_9
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 programming language with built-in specification constructs
A proof checker for unSAT proofs
Computer-Aided Cryptographic Proofs
Testing program for EasyCrypt formalizations
A 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
eprovereprover
Automated theorem prover for full first-order logic with equality
eprovereprover-ho
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
An automated first-order logic theorem prover
isabelleisabelle
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)
Automatic and interactive theorem prover
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
Draw SVG digital circuits schematics from yosys JSON netlists
A new symbolic model checker for the analysis of synchronous finite-state and infinite-state syste…
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
SAT solver binary based on the msat library
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
A fast solver for the #SAT model counting problem