Projects

Complexity Theory of Solvers

The Complexity Theory of Solvers project aims to bridge the practice and theory of SAT.

Crypto-SAT

The Crypto-SAT project aims to enhance SAT solvers for cryptanalysis tasks, tailoring solver-internal components to improve performance on cryptographic instances.

Z3 String Solver

The 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. Z3 string solver is implemented as a string theory plug-in of the powerful Z3 SMT solver.

MathCheck

MathCheck is a combination of the computer algebra system (CAS) SAGE with a SAT Solver. Users can define predicates in the language of the CAS which can be finitely verified in a loop by the SAT solver, analogous to basic SMT approaches.

STP

STP is a constraint solver (or SMT solver) aimed at solving constraints of bitvectors and arrays. These types of constraints can be generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers, model checkers, and by many other applications.

The Maple series of solvers provides efficient behind-the-scenes reasoning for STP.