Hlavní stránka > Výsledky hledání: Hečko, Michal
Hledej:
Tipy pro vyhledávaní :: Rozšířené hledání
Hledej ve sbírkách:
Seřadit podle: Zobrazit výsledky: Výstupní formát:
Národní úložiště šedé literatury Nalezeno 2 záznamů.  Hledání trvalo 0.00 vteřin. 
An Automata-Based Decision Procedure
 Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
Úplný záznam
An Automata-Based Decision Procedure
 Hečko, Michal ; Češka, Milan (oponent) ; Lengál, Ondřej (vedoucí práce)
Presburger arithmetics (PrA) is a decidable, first-order theory of natural numbers, with applications in many areas in formal verification of software properties. SMT-solvers tools implementing various algorithmic approaches to deciding whether a formula has a solution play a crucial role in formal verification. In this work, we document building a novel automatic SMT solver for PrA based on finite automata an approach that no SMT solver currently employs. We provide an overview of challenges and their solutions arising from the complexity of such a tool, including results from the conducted experiments already showing problems in which this alternative approach outperforms the state-of-the-art solvers. We have also identified problems in which the performance of the automata-based procedure struggles, which are open research opportunities.
Úplný záznam

Viz též: podobná jména autorů
1 Hečko, Miroslav
Chcete být upozorněni, pokud se objeví nové záznamy odpovídající tomuto dotazu?
Přihlásit se k odběru RSS.
Digitální repozitář :: Hledej :: Nový záznam :: Personalizace :: Nápověda
Powered by Invenio v1.1.2
Spravuje admin.invenio@techlib.cz
Tato stránka je dostupná také v následujících jazycích:
Česky  English