Sloth: An SMT Solver for String Constraints
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F18%3APR29285" target="_blank" >RIV/00216305:26230/18:PR29285 - isvavai.cz</a>
Výsledek na webu
<a href="http://www.fit.vutbr.cz/research/prod/index.php?id=563" target="_blank" >http://www.fit.vutbr.cz/research/prod/index.php?id=563</a>
DOI - Digital Object Identifier
—
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Sloth: An SMT Solver for String Constraints
Popis výsledku v původním jazyce
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ázev v anglickém jazyce
Sloth: An SMT Solver for String Constraints
Popis výsledku anglicky
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.
Klasifikace
Druh
R - Software
CEP obor
—
OECD FORD obor
20206 - Computer hardware and architecture
Návaznosti výsledku
Projekt
Výsledek vznikl pri realizaci vícero projektů. Více informací v záložce Projekty.
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)
Ostatní
Rok uplatnění
2018
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Interní identifikační kód produktu
sloth
Technické parametry
Pro informace o licenčních podmínkách prosím kontaktujte: Mgr. Radka Báčová, Výzkumné centrum informačních technologií, Fakulta informačních technologií VUT v Brně, Božetěchova 2, 612 66 Brno, 541 141 473.
Ekonomické parametry
Software je volně dostupný včetně zdrojových textů.
IČO vlastníka výsledku
—
Název vlastníka
Fakulta informačních technologií