Showing entries 1-62 out of 62.
Interactive theorem prover
AIGER model checking for Property Directed Reachability
Interactive theorem-prover and dependently typed programming language, based on extrinsic (aka Cur…
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_20
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
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
Computer-Aided Cryptographic Proofs
Testing program for EasyCrypt formalizations
Automated first-order 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
Modern, parallel SAT solver (sequential version)
Modern, parallel SAT solver (parallel version)
Interactive theorem prover based on Higher-Order Logic
Symbolic virtual machine built on top of LLVM
High-performance typed higher order prover
Automated theorem prover for classical higher-order logic with choice
Program for proof-tree visualization
Automated theorem prover for higher-order logic
Automated theorem prover for first-order logic
Verification of stateful processes (via Proverif)
Security protocol verification in the symbolic model
IDE for the TLA+ tools
tlaplustlaplus
Algorithm specification language with model checking tools
tlaplustlaplus18
Algorithm specification language with model checking tools
Mechanically check TLA+ proofs
Vampire Theorem Prover
Open, trustable and efficient SMT-solver
Platform for deductive program verification
High-performance theorem prover and SMT solver
z3z3
High-performance theorem prover and SMT solver
z3z3_4_11
High-performance theorem prover and SMT solver
z3z3_4_12
High-performance theorem prover and SMT solver
z3z3_4_8_5
High-performance theorem prover and SMT solver
High-performance theorem prover and SMT solver
High-performance theorem prover and SMT solver
High-performance theorem prover and SMT solver
High-performance theorem prover and SMT solver
TPTP wrapper for Z3 prover