Sloth: An SMT Solver for String Constraints

Lenochod - SMT solver pro řetězcová omezení

software

In order to use the result by another entity, it is always necessary to acquire a license

The licensor does not require a license fee for the result

Holík Lukáš, doc. Mgr., Ph.D. (DITS)
Janků Petr, Ing. (RG VERIFIT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
Lin Anthony (FIT)
Rummer Philipp

Alternating Finite Automata, Decision Procedure, IC3, String Solving

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.

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

Free software under the terms of GNU GPLv3 (cf.http://www.gnu.org/licenses/gpl.html).

AQUAS: Aggregated Quality Assurance for Systems, EU, Horizon 2020, 8A17001, 737475, 2017-2020, completed
Bezpečné a spolehlivé počítačové systémy, BUT, Vnitřní projekty VUT, FIT-S-17-4014, 2017-2020, completed
Efficient Automata for Formal Reasoning, GACR, Juniorské granty, GJ16-24707Y, 2016-2018, running
IT4Innovations excellence in science, MŠMT, Národní program udržitelnosti II, LQ1602, 2016-2020, completed
ROBUST - veRificatiOn and Bug hUnting for advanced SofTware, GACR, Standardní projekty, GA17-12465S, 2017-2019, running

Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)

Department of Intelligent Systems (DITS)