Project Details

Efficient Automata Techniques 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. (UITS FIT VUT) , research leader
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Šimáček Jiří, Ing., Ph.D. (UITS FIT VUT)
Publications

2020

  • ČEŠKA Milan, HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Approximate Reduction of Finite Automata for High-Speed Network Intrusion Detection. International Journal on Software Tools for Technology Transfer, vol. 22, no. 5, 2020, pp. 523-539. ISSN 1433-2779. Detail
  • HOLÍK Lukáš, JANKŮ Petr, LIN Anthony W., RUMMER Philipp and 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 and VOJNAR Tomáš. Nested Antichains for WS1S. Acta Informatica, vol. 56, no. 3, 2019, pp. 205-228. ISSN 0001-5903. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., CHEN Yu-Fang, BUI Phi Diep, HOLÍK Lukáš, REZINE Ahmed and 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, pp. 165-169. ISBN 978-0-9835678-8-2. Detail

2018

  • HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus and VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata. In: Proc. of 16th International Symposium on Automated Technology for Verification and Analysis. Heidelberg: Springer Verlag, 2018, pp. 109-125. ISBN 978-3-030-01089-8. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, LENGÁL Ondřej, SÍČ Juraj, VEANES Margus and VOJNAR Tomáš. Simulation Algorithms for Symbolic Automata (Technical Report). Ithaca, 2018. Detail
  • HOLÍK Lukáš, JANKŮ Petr, LIN Anthony W., RUMMER Philipp and VOJNAR Tomáš. String constraints with concatenation and transducers solved efficiently. Proceedings of the ACM on Programming Languages, vol. 2, no. 2, 2018, pp. 96-127. ISSN 2475-1421. Detail

2017

  • HOLÍK Lukáš, HRUŠKA Martin, LENGÁL Ondřej, ROGALEWICZ Adam and VOJNAR Tomáš. Counterexample Validation and Interpolation-Based Refinement for Forest Automata. In: Proceedings of VMCAI'17. Lecture Notes in Computer Science, vol. 10145. Cham: Springer Verlag, 2017, pp. 288-309. ISBN 978-3-319-52234-0. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, MEYER Roland, VOJNAR Tomáš and WOLF Sebastian. Effect Summaries for Thread-Modular Analysis. In: SAS 2017: Static Analysis. Lecture Notes in Computer Science, vol. 10422. Cham: Springer International Publishing, 2017, pp. 169-191. ISBN 978-3-319-66706-5. ISSN 0302-9743. Detail
  • LENGÁL Ondřej, LIN Anthony W., MAJUMDAR Rupak and RUMMER Philipp. Fair Termination for Parameterized Probabilistic Concurrent Systems. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 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 and 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, pp. 602-617. ISBN 978-1-4503-4988-8. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. In: Proceedings of TACAS'17. Lecture Notes in Computer Science, vol. 10205. Heidelberg: Springer Verlag, 2017, pp. 407-425. ISBN 978-3-662-54576-8. ISSN 0302-9743. Detail
  • FIEDOR Tomáš, HOLÍK Lukáš, JANKŮ Petr, LENGÁL Ondřej and VOJNAR Tomáš. Lazy Automata Techniques for WS1S. arXiv:1701.06282, 2017. Detail
  • ČEŠKA Milan, ČEŠKA Milan and PAOLETTI Nicola. 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, pp. 38-46. ISBN 978-3-319-74726-2. Detail
  • LAURENTI Luca, ABATE Alessandro, BORTOLUSSI Luca, CARDELLI Luca, ČEŠKA Milan and 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, pp. 55-64. ISBN 978-1-4503-4590-3. Detail

2016

  • ALDEGHERI Stefano, BARNAT Jiří, BOMBIERI Nicola, BUSATO Federico and Č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, vol. 10104. Cham: Springer Verlag, 2016, pp. 519-531. ISBN 978-3-319-58942-8. Detail
  • ČEŠKA Milan, PILAŘ Petr, PAOLETTI Nicola, BRIM Luboš and 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, vol. 9636. Berlin: Springer International Publishing, 2016, pp. 367-384. ISBN 978-3-662-49673-2. ISSN 0302-9743. Detail
  • ALMEIDA Ricardo, HOLÍK Lukáš and 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, pp. 717-735. ISBN 978-3-662-49673-2. Detail
  • HOLÍK Lukáš, MEYER Roland and 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, pp. 41-57. ISBN 978-3-95977-027-9. Detail
Products

2018

  • Sloth: An SMT Solver for String Constraints, software, 2018
    Authors: Holík Lukáš, Janků Petr, Lin Anthony W., Rummer Philipp, Vojnar Tomáš Detail

2017

  • Gaston - Symbolic WS1S Solver, software, 2017
    Authors: Fiedor Tomáš, Holík Lukáš, Janků Petr, Lengál Ondřej, Vojnar Tomáš Detail
Back to top