Přístupnostní navigace
E-application
Search Search Close
Project detail
Duration: 01.01.2016 — 31.12.2018
Funding resources
Czech Science Foundation - Juniorské granty
- whole funder (2016-01-01 - 2018-12-31)
On the project
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.
Description in CzechProjekt 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í.
Keywordsfinite automata formal verification logics decision procedures string analysis shape analysis parallelism concurrency context-free languages SAT SMT
Key words in Czechkonečné automaty formální verifikace logiky rozhodovací procedury programy s řetězci paralelní programy ukazatelové programy bezkontextové jazyky SAT SMT
Mark
GJ16-24707Y
Default language
English
People responsible
Lengál Ondřej, Ing., Ph.D. - fellow researcherŠimáček Jiří, Ing., Ph.D. - fellow researcherHolík Lukáš, doc. Mgr., Ph.D. - principal person responsible
Units
Department of Intelligent Systems- beneficiary (2015-03-26 - 2018-12-31)
Results
Č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
Č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
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.; 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.; 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
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
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
Č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
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
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.; 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
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
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.; 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
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
Č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
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
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.; JANKŮ, P.; VOJNAR, T.; LIN, A.; RUMMER, P.: sloth; Sloth: An SMT Solver for String Constraints. Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/sloth/ (http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/) a https://github.com/uuverifiers/sloth. URL: https://www.fit.vut.cz/research/product/563/. (software)Detail
FIEDOR, T.; HOLÍK, L.; JANKŮ, P.; LENGÁL, O.; VOJNAR, T.: gaston; Gaston - Symbolic WS1S Solver. Nástroj a dodatečné informace se nacházejí na http://www.fit.vutbr.cz/research/groups/verifit/tools/gaston/ a https://github.com/tfiedor/gaston. URL: https://www.fit.vut.cz/research/product/511/. (software)Detail