Detail projektu

Efficient Automata Techniques for Formal Reasoning

Období řešení: 1. 1. 2016 - 31. 12. 2018

Typ projektu: grant

Kód: GJ16-24707Y

Agentura: Grantová agentura České republiky

Program: Juniorské granty

Název česky
Efektivní automaty pro formální rozhodování
Typ
grant
Klíčová slova

konečné automaty
formální verifikace
logiky
rozhodovací procedury
programy s řetězci
paralelní programy
ukazatelové programy
bezkontextové jazyky
SAT
SMT

Abstrakt

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í.

Řešitelé
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT) , hlavní řešitel
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Publikace

2020

  • Č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, roč. 22, č. 5, 2020, s. 523-539. ISSN 1433-2779. Detail
  • HOLÍK Lukáš, JANKŮ Petr, LIN Anthony W., RUMMER Philipp a VOJNAR Tomáš. String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report). New York: Springer International Publishing, 2020. Detail

2019

  • FIEDOR Tomáš, HOLÍK Lukáš, LENGÁL Ondřej a VOJNAR Tomáš. Nested Antichains for WS1S. Acta Informatica, roč. 56, č. 3, 2019, s. 205-228. ISSN 0001-5903. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., CHEN Yu-Fang, BUI Phi Diep, HOLÍK Lukáš, 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. 165-169. ISBN 978-0-9835678-8-2. Detail

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. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus a VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca, 2018. Detail
  • 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, roč. 2, č. 2, 2018, s. 96-127. ISSN 2475-1421. Detail

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. Lecture Notes in Computer Science, roč. 10145. Cham: Springer Verlag, 2017, s. 288-309. ISBN 978-3-319-52234-0. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, MEYER Roland, VOJNAR Tomáš a WOLF Sebastian. Effect Summaries for Thread-Modular Analysis Sound Analysis Despite an Unsound Heuristic. In: SAS 2017: Static Analysis. Lecture Notes in Computer Science, roč. 10422. Cham: Springer International Publishing, 2017, s. 169-191. ISBN 978-3-319-66706-5. ISSN 0302-9743. Detail
  • LENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak a RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, roč. 10205. Heidelberg: Springer Verlag, 2017, s. 499-517. ISBN 978-3-662-46680-3. ISSN 0302-9743. Detail
  • ABDULLA 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. ACM. New York: Association for Computing Machinery, 2017, s. 602-617. ISBN 978-1-4503-4988-8. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej a VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, roč. 10205. Heidelberg: Springer Verlag, 2017, s. 407-425. ISBN 978-3-662-54576-8. ISSN 0302-9743. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej a VOJNAR Tomáš. Lazy Automata Techniques for WS1S. arXiv:1701.06282, 2017. Detail
  • ČEŠKA Milan, ČEŠKA Milan a PAOLETTI Nicola. Precise Parameter Synthesis for Generalised Stochastic Petri Nets with Interval Parameters. In: Proceedings of 16th International Conference on Computer Aided Systems Theory. LNCS volume 10672. Heidelberg: Springer Verlag, 2017, s. 38-46. ISBN 978-3-319-74726-2. Detail
  • 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. ACM. New York: Association for Computing Machinery, 2017, s. 55-64. ISBN 978-1-4503-4590-3. Detail

2016

  • ALDEGHERI 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. Lecture Notes in Computer Science, roč. 10104. Cham: Springer Verlag, 2016, s. 519-531. ISBN 978-3-319-58942-8. Detail
  • Č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. Lecture Notes in Computer Science, roč. 9636. Berlin: Springer International Publishing, 2016, s. 367-384. ISBN 978-3-662-49673-2. ISSN 0302-9743. Detail
  • ALMEIDA Ricardo, HOLÍK Lukáš a MAYR Richard. Reduction of Nondeterministic Tree Automata. In: Tools and Algorithms for the Construction and Analysis of Systems. Volume 9636 of the series Lecture Notes in Computer Science. Berlin Heidelberg: Springer Verlag, 2016, s. 717-735. ISBN 978-3-662-49673-2. Detail
  • 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). Leibniz International Proceedings in Informatics (LIPIcs). Dagstuhl: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2016, s. 41-57. ISBN 978-3-95977-027-9. Detail
Produkty

2018

  • Lenochod - SMT solver pro řetězcová omezení, software, 2018
    Autoři: Holík Lukáš, Janků Petr, Lin Anthony W., Rummer Philipp, Vojnar Tomáš Detail

2017

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