Human Folly about “SMT-COMP”

index

SMTInterpol (smt-comp.github.io):
#SMT-COMP #PDF #paper about #SMTInterpol, a DPLL(T)/CDCL #SMT solver in Java licensed under LGPLv3. #toread #formal-methods #SAT
on 02024-06-16
(cvc5.github.io):
"CVC5" (Cooperating Validity Checker 5), based on #Minisat, written in C++, and licensed under a 3-clause BSD license, is kind of the top #SMT solver according to the #SMT-COMP results. You can hook it up to #ABC, #CryptoMiniSat, #libpoly, #GMP, #CaDiCal, #symfpu, #CLN (the Class Library for Numbers), and #GLPK. #toread #formal-methods #SAT
on 02024-06-16
CVC5 (smt-comp.github.io):
#SMT-COMP #PDF #paper about the #CVC5 CDCL(T) #SMT solver, the top winner in many categories, licensed under a BSD license. #SAT #formal-methods #toread
on 02024-06-16
iProver (smt-comp.github.io):
#SMT-COMP #PDF #paper about #iProver. #toread #formal-methods #SMT #SAT
on 02024-06-16
iProver (gitlab.com):
#SMT-COMP winner "iProver" is a first-order theorem prover written in OCaml licensed under GPL2+. It wraps #Z3 and #Minisat #SAT solvers. #formal-methods #SMT
on 02024-06-16
(vprover.github.io):
#SMT-COMP winner "Vampire" is under a 3-clause BSD license. #SMT #SAT #formal-methods
on 02024-06-16
Vampire (smt-comp.github.io):
#SMT-COMP #PDF #paper about #Vampire, a first-order theorem prover. #toread #formal-methods #SMT #SAT
on 02024-06-16
(yices.csl.sri.com):
#SMT-COMP winner "Yices2" #SMT #SAT #formal-methods
on 02024-06-16
Yices2 (smt-comp.github.io):
#PDF #SMT-COMP paper about the #Yices2 CDCL(T) #SMT solver, which supports three different #SAT solver backends: CaDiCaL, CryptoMiniSat, and Kissat. #formal-methods
on 02024-06-16
(bitwuzla.github.io):
The "Bitwuzla" #SMT solver, one of the 02023 #SMT-COMP winners, is also under an MIT license. #formal-methods
on 02024-06-16
Bitwuzla (smt-comp.github.io):
#PDF #paper about the #Bitwuzla #SMT solver at #SMT-COMP, a C++ rewrite of a fork of Boolector. #SAT #toread #formal-methods
on 02024-06-16
Z3Pp (github.com):
The "Z3++" #SMT solver, based on #Z3, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16
OpenSMT (github.com):
The "OpenSMT" #SMT (#SAT plus theories) solver, one of the 02023 #SMT-COMP winners, under basically an MIT license #formal-methods
on 02024-06-16
Results (smt-comp.github.io):
#SMT and #SAT competition "SMT-COMP" has many divisions now. #formal-methods
on 02024-06-16