Faculty of Information Technology, BUT

Product Details

Sloth: An SMT Solver for String Constraints

Created: 2018

Czech title
Lenochod - SMT solver pro řetězcová omezení
Type
software
License
required - free
Authors
Holík Lukáš, Mgr., Ph.D. (DITS FIT BUT)
Janků Petr, Ing. (DITS FIT BUT)
Lin Anthony W. (UOx)
Rummer Philipp (Uppsala)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Keywords
Alternating Finite Automata, Decision Procedure, IC3, String Solving
Description
Sloth is a decision procedure for several relevant fragments of string constraints, including the straight-line fragment and acyclic formulas. In contrast to most other string solvers, Sloth is able to decide satisfiability of constraints combining concatenation, regular expressions, and transduction, all of which are essential in applications. 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.
Location
Licence
Free software under the terms of GNU GPLv3 (cf.http://www.gnu.org/licenses/gpl.html).
Back to top