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

2018Lenochod - SMT solver pro řetězcová omezení, software, 2018
Autoři: Holík Lukáš, Janků Petr, Lin Anthony W., Rummer Philipp, Vojnar Tomáš
2017Gaston - Symbolická WS1S Rozhodovací Procedura, software, 2017
Autoři: Fiedor Tomáš, Holík Lukáš, Janků Petr, Lengál Ondřej, Vojnar Tomáš

Publikace

2019ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed a RUMMER Philipp. Trau: SMT solver for string constraints. In: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2019, s. 1-5. ISBN 978-0-9835678-8-2.
 ČEŠKA Milan, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. International Journal on Software Tools for Technology Transfer. 2019, roč. 2019, č. 1, s. 1-17. ISSN 1433-2779.
 FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Nested Antichains for WS1S. Acta Informatica. 2019, roč. 56, č. 3, s. 205-228. ISSN 0001-5903.
2018HOLÍK Lukáš a TUROŇOVÁ Lenka. Towards Smaller Invariants for Proving Coverability. In: Computer Aided Systems Theory - EUROCAST 2017. Berlin Heidelberg: Springer Verlag, 2018, s. 109-116. ISBN 978-3-319-74727-9.
 HOLÍK Lukáš, JANKŮ Petr, LIN Anthony W., RUMMER Philipp a VOJNAR Tomáš. String constraints with concatenation and transducers solved efficiently. Proceedings of the ACM on Programming Languages. New York: Association for Computing Machinery, 2018, roč. 2018, č. 2, s. 96-127. ISSN 2475-1421.
 HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus a VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca, 2018.
 HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus a VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata. In: Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Heidelberg: Springer Verlag, 2018, s. 109-125. ISBN 978-3-030-01089-8. ISSN 0302-9743.
2017ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, REZINE Ahmed a RUMMER Philipp. Flatten and conquer: a framework for efficient analysis of string constraints. In: Proceedings of the 38th ACM SIGPLAN Conference on Programming Language Design and Implementation. New York: Association for Computing Machinery, 2017, s. 602-617. ISBN 978-1-4503-4988-8.
 ČEŠKA Milan, ČEŠKA Milan a PAOLETTI Nicola. Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters. In: Proceedings of 16th International Conference on Computer Aided Systems Theory. Heidelberg: Springer Verlag, 2017, s. 38-46. ISBN 978-3-319-74727-9.
 FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej a VOJNAR Tomáš. Lazy Automata Techniques for WS1S. arXiv:1701.06282, 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. ISSN 0302-9743.
 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. ISSN 0302-9743.
 HOLÍK Lukáš, MEYER Roland, VOJNAR Tomáš a WOLF Sebastian. Effect Summaries for Thread-Modular Analysis. In: SAS 2017: Static Analysis. Cham: Springer International Publishing, 2017, s. 169-191. ISBN 978-3-319-66706-5.
 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. ISSN 0302-9743.
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: 18.232.53.231