Vše

Co hledáte?

Vše
Projekty
Výsledky výzkumu
Subjekty

Rychlé hledání

  • Projekty podpořené TA ČR
  • Významné projekty
  • Projekty s nejvyšší státní podporou
  • Aktuálně běžící projekty

Chytré vyhledávání

  • Takto najdu konkrétní +slovo
  • Takto z výsledků -slovo zcela vynechám
  • “Takto můžu najít celou frázi”

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í