Project Details

Efficient Automata for Formal Reasoning

Project Period: 1. 1. 2016 – 31. 12. 2018

Project Type: grant

Code: GJ16-24707Y

Agency: Czech Science Foundation

Program: Juniorské granty

Czech title
Efektivní automaty pro formální rozhodování
Type
grant
Keywords

finite automata
formal verification
logics
decision procedures
string analysis
shape analysis
parallelism
concurrency
context-free languages
SAT
SMT

Abstract

The project focuses on development of efficient algorithms for finite automata
applicable in formal verification and analysis of dynamic systems. The central
idea is to explore connections between automata, SAT/SMT solving, and program
verification. We believe that because all these three domains solve similar
problems, interchanging ideas between the domains is possible and may
significantly advance not only the domain of automata but also the other
mentioned areas. The automata-based algorithms developed in the project will in
particular target the following four lively domains of applications: analysis of
string manipulating programs, shape analysis, verification of concurrent
programs, and decision procedures of selected logics suitable for verification of
infinite-state systems (such as WSkS or separation logic). The work on the
project will include rigorous mathematical description of the developed
principles and algorithms, as well as their implementation and experimental
evaluation.

Team members
Holík Lukáš, doc. Mgr., Ph.D. (DITS) – research leader
Lengál Ondřej, Ing., Ph.D. (DITS)
Šimáček Jiří, Ing., Ph.D.
Publications

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 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. 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 Sound Analysis Despite an Unsound Heuristic. 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
Back to top