Related Tools

MapleSAT

MapleSAT is the main CDCL SAT solver that we have used in our works, both in MaplePainless as a backend solver and in CDCL(Crypto) as the main instrumented solver with programmatic interfaces. The key innovation of the Maple series of solvers is the use of the learning rate branching heuristic (LRB), a departure from the VSIDS branching heuristic that has been the status quo for the past decade of SAT solving.

MathCheck

MathCheck is a system which combines functionality from Boolean satisfiability (SAT) solvers and computer algebra systems (CAS) to verify conjectures in mathematics up to a finite bound and to search for counterexamples. This architecture queries CAS through a programmatic interface similar to our algebraic fault analysis.

Z3 String Solver

Z3 string solver is a constraint solver for the quantifier-free theory of string equations, the regular-expression membership predicates, and linear arithmetic over the length functions. Z3str3 is implemented as a string theory plug-in of the powerful Z3 SMT solver.