Detail výsledku
Sloth: An SMT Solver for String Constraints
Janků Petr, Ing., Ph.D.
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Lin Anthony, FIT (FIT)
Rummer Philipp
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.
Alternating Finite Automata, Decision Procedure, IC3, String Solving
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
Bezpečné a spolehlivé počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-17-4014, zahájení: 2017-03-01, ukončení: 2020-02-29, ukončen
Efektivní automaty pro formální rozhodování, GAČR, Juniorské granty, GJ16-24707Y, zahájení: 2016-01-01, ukončení: 2018-12-31, ukončen
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, zahájení: 2016-01-01, ukončení: 2020-12-31, ukončen
ROBUST - Verifikace a hledání chyb v pokročilém softwaru, GAČR, Standardní projekty, GA17-12465S, zahájení: 2017-01-01, ukončení: 2019-12-31, ukončen