An SMT Solver for strings
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.


An SMT Solver for String Constraints

Sloth is a decision procedure for several relevant fragments of string constraints, including the straight-line fragment, which is sufficiently expressive for many applications from verification or security. Sloth uses succinct alternating finite-state automata (AFAs) as concise symbolic representations of string constraints, and uses model checking algorithms like IC3 for solving emptiness of the AFA.

For documentation, see