Related Tools

Constraint Generation / Conversion Tools

StringFuzz

StringFuzz is an instance transformer and generator for SMT-LIB instances with string and regex constraints.

regex2smtlib

regex2smtlib is a tool developed by Julian Thomé for generating constraints in SMT-LIB format from Perl-compatible regular expressions.

Related Solvers

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.

MapleSAT

The MapleSAT series of SAT solvers are a family of conflict-driven clause-learning SAT solvers for solving the Boolean satisfiability problem. The key innovation of these 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.

STP

STP is a constraint solver for the theory of quantifier-free bit-vectors that can solve many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers.

Hampi

Hampi is a solver for string constraints. Hampi is designed for constraints generated by program analysis tools, automated bug finders, and intelligent fuzzers.
Hampi constraints express membership in regular languages and bounded context-free languages. Hampi constraints may contain context-free-language definitions, regular-language definitions and operations, and the membership predicate. Given a set of constraints, Hampi outputs a string that satisfies all the constraints, or reports that the constraints are unsatisfiable.