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 https://github.com/uuverifiers/sloth/wiki