Detail produktu

Sloth: An SMT Solver for String Constraints

HOLÍK, L. JANKŮ, P. VOJNAR, T. LIN, A. RUMMER, P.

Typ produktu

software

Abstrakt

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.

Klíčová slova

Alternating Finite Automata, Decision Procedure, IC3, String Solving

Datum vzniku

5. 3. 2018

Umístění

Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/sloth/ (http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/) a https://github.com/uuverifiers/sloth

Možnosti využití

K využití výsledku jiným subjektem je vždy nutné nabytí licence

Licenční poplatek

Poskytovatel licence na výsledek nepožaduje licenční poplatek

www