Efficient Automata Techniques for Formal Reasoning

Název v češtině:Efektivní automaty pro formální rozhodování
Hlavní řešitel:Holík Lukáš
Další řešitelé:Lengál Ondřej, Šimáček Jiří
Agentura:Grantová agentura České republiky - Juniorské granty
Kód:GJ16-24707Y
Zahájení:2016-01-01
Ukončení:2018-12-31
Klíčová slova:konečné automaty
formální verifikace
logiky
rozhodovací procedury
programy s řetězci
paralelní programy
ukazatelové programy
bezkontextové jazyky
SAT
SMT
Anotace:
Projekt si klade za cíl vyvinout nové efektivní a praktické algoritmy pro konečné automaty aplikovatelné ve formální verifikaci a analýze dynamických systémů. Bude stavět zejména na studiu souvislostí mezi automatovými problémy, metodami řešení SAT/SMT problémů a formální verifikací. Věříme, že hlubší porozumění spojitostí mezi metodami používanými v těchto oblastech posune vpřed nejen oblast automatových technik s aplikacemi ve verifikaci, ale také ostatní zmíněné oblasti. Vyvíjené algoritmy budou konkrétně zaměřeny zejména na aplikace automatů v analýze programů s řetězci, verifikaci programů s ukazateli, analýze paralelních programů a v rozhodovacích procedurách logik souvisejících s formální verifikací nekonečně stavových systémů, jako jsou WSkS nebo separační logika. Práce na projektu zahrne rigorózní matematický popis navrhovaných metod a studium jejich teoretických vlastností, ale také jejich experimentální implementaci a vyhodnocení.

Produkty

2017Gaston - Symbolická WS1S Rozhodovací Procedura, software, 2017
Autoři: Fiedor Tomáš, Holík Lukáš, Janků Petr, Lengál Ondřej, Vojnar Tomáš

Publikace

2017ABDULLA Parosh A., HAZIZA Frédéric, HOLÍK Lukáš, JONSSON Bengt a REZINE Ahmed. An integrated specification and verification technique for highly concurrent data structures for highly concurrent data structures. International Journal on Software Tools for Technology Transfer. 2017, roč. 5, č. 19, s. 549-563. ISSN 1433-2779.
 ČEŠKA Milan, ČEŠKA Milan a PAOLETTI Nicola. Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters. Processing of Sixteenth International Conference on Computer Aided Systems Theory (Extended Abstract). Las Palmas de Gran Canaria, 2017.
 FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej a VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, s. 407-425. ISBN 978-3-662-54576-8.
 FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej a VOJNAR Tomáš. Lazy Automata Techniques for WS1S. arXiv:1701.06282, 2017.
 HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam a VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Cham: Springer Verlag, 2017, s. 288-309. ISBN 978-3-319-52234-0.
 LAURENTI Luca, ABATE Alessandro, BORTOLUSSI Luca, CARDELLI Luca, ČEŠKA Milan a KWIATKOWSKA Marta. Reachability Computation for Switching Diffusions:Finite Abstractions with Certifiable and Tuneable Precision. In: Proceedings of the 20th ACM International Conference on Hybrid Systems: Computation and Control. New York: Association for Computing Machinery, 2017, s. 55-64. ISBN 978-1-4503-4590-3.
 LENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak a RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Heidelberg: Springer Verlag, 2017, s. 499-517. ISBN 978-3-662-46680-3.
2016ALDEGHERI Stefano, BARNAT Jiří, BOMBIERI Nicola, BUSATO Federico a ČEŠKA Milan. Parametric Multi-Step Scheme for GPU-Accelerated Graph Decomposition into Strongly Connected Components. In: Proceedings of 2nd Workshop on Performance Engineering for Large Scale Graph Analytics. Cham: Springer Verlag, 2016, s. 519-531. ISBN 978-3-319-58942-8.
 ALMEIDA Ricardo, HOLÍK Lukáš a MAYR Richard. Reduction of Nondeterministic Tree Automata. In: Tools and Algorithms for the Construction and Analysis of Systems. Berlin Heidelberg: Springer Verlag, 2016, s. 717-735. ISBN 978-3-662-49673-2.
 ČEŠKA Milan, PILAŘ Petr, PAOLETTI Nicola, BRIM Luboš a KWIATKOWSKA Marta. PRISM-PSY: Precise GPU-Accelerated Parameter Synthesis for Stochastic Systems. In: Proceedings of the 22nd International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Berlin: Springer International Publishing, 2016, s. 367-384. ISBN 978-3-662-49673-2. ISSN 0302-9743.
 HOLÍK Lukáš, MEYER Roland a MUSKALLA Sebastian. Summaries for Context-Free Games. In: 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016, s. 41-57. ISBN 978-3-95977-027-9.

Vaše IPv4 adresa: 54.91.38.173
Přepnout na IPv6 spojení

DNSSEC [dnssec]