Detail projektu

Efficient Automata 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) – hlavní řešitel
Lengál Ondřej, Ing., Ph.D. (UITS)
Šimáček Jiří, Ing., Ph.D.
Publikace

2020

  • ČEŠKA, M.; HAVLENA, V.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. International Journal on Software Tools for Technology Transfer, 2020, vol. 22, no. 5, p. 523-539. ISSN: 1433-2779. Detail
  • HOLÍK, L.; JANKŮ, P.; VOJNAR, T.; LIN, A.; RUMMER, P. String Constraints with Concatenation and Transducers Solved Efficiently (Technical Report). New York: Springer International Publishing, 2020. p. 1-33. Detail

2019

  • ABDULLA, P.; ATIG, M.; CHEN, Y.; BUI PHI, D.; HOLÍK, L.; REZINE, A.; RUMMER, P. Trau: SMT solver for string constraints. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2019. p. 165-169. ISBN: 978-0-9835678-8-2. Detail
  • FIEDOR, T.; HOLÍK, L.; LENGÁL, O.; VOJNAR, T. Nested Antichains for WS1S. Acta Informatica, 2019, vol. 56, no. 3, p. 205-228. ISSN: 0001-5903. Detail

2018

  • HOLÍK, L.; JANKŮ, P.; VOJNAR, T.; LIN, A.; RUMMER, P. String constraints with concatenation and transducers solved efficiently. Proceedings of the ACM on Programming Languages, 2018, vol. 2, no. 2, p. 96-127. ISSN: 2475-1421. Detail
  • HOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca: 2018. p. 1-23. Detail
  • HOLÍK, L.; LENGÁL, O.; SÍČ, J.; VOJNAR, T.; VEANES, M. Simulation Algorithms for Symbolic Automata. In Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2018. p. 109-125. ISBN: 978-3-030-01089-8. ISSN: 0302-9743. Detail

2017

  • ČEŠKA, M.; ČEŠKA, M.; PAOLETTI, N. Precise Parameter Synthesis for Stochastic Petri Nets with Interval Rate Parameters. In Proceedings of 16th International Conference on Computer Aided Systems Theory. LNCS volume 10672. Heidelberg: Springer Verlag, 2017. p. 38-46. ISBN: 978-3-319-74726-2. Detail
  • FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. arXiv:1701.06282: 2017. p. 0-0. Detail
  • FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T. Lazy Automata Techniques for WS1S. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 407-425. ISBN: 978-3-662-54576-8. ISSN: 0302-9743. Detail
  • HOLÍK, L.; ABDULLA, P.; ATIG, M.; BUI PHI, D.; CHEN, Y.; REZINE, A.; RUMMER, P. 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. p. 602-617. ISBN: 978-1-4503-4988-8. Detail
  • HOLÍK, L.; HRUŠKA, M.; LENGÁL, O.; ROGALEWICZ, A.; VOJNAR, T. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In Proceedings of VMCAI'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Cham: Springer Verlag, 2017. p. 288-309. ISBN: 978-3-319-52234-0. ISSN: 0302-9743. Detail
  • HOLÍK, L.; MEYER, R.; VOJNAR, T.; WOLF, S. Effect Summaries for Thread-Modular Analysis. In SAS 2017: Static Analysis. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Cham: Springer International Publishing, 2017. p. 169-191. ISBN: 978-3-319-66706-5. ISSN: 0302-9743. Detail
  • LAURENTI, L.; ABATE, A.; BORTOLUSSI, L.; CARDELLI, L.; ČEŠKA, M.; KWIATKOWSKA, M. 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. p. 55-64. ISBN: 978-1-4503-4590-3. Detail
  • LENGÁL, O.; LIN, A.; MAJUMDAR, R.; RUMMER, P. Fair Termination for Parameterized Probabilistic Concurrent Systems. In Proceedings of TACAS'17. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2017. p. 499-517. ISBN: 978-3-662-46680-3. ISSN: 0302-9743. Detail

2016

  • ČEŠKA, M.; ALDEGHERI, S.; BARNAT, J.; BOMBIERI, N.; BUSATO, F. 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. Cham: Springer Verlag, 2016. p. 519-531. ISBN: 978-3-319-58942-8. Detail
  • ČEŠKA, M.; PILAŘ, P.; PAOLETTI, N.; BRIM, L.; KWIATKOWSKA, M. 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. Lecture Notes in Computer Science. Berlin: Springer International Publishing, 2016. p. 367-384. ISBN: 978-3-662-49673-2. ISSN: 0302-9743. Detail
  • HOLÍK, L.; ALMEIDA, R.; MAYR, R. 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. p. 717-735. ISBN: 978-3-662-49673-2. Detail
  • HOLÍK, L.; MEYER, R.; MUSKALLA, S. 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. p. 41-57. ISBN: 978-3-95977-027-9. Detail
Nahoru