Project Details

AUTODEV - Automaty v rozhodovacích procedurách a verifikaci

Project Period: 1. 1. 2019 - 31. 12. 2021

Project Type: grant

Code: GA19-24397S

Agency: Czech Science Foundation

Program: Standardní projekty

English title
Automata for Decision Procedures and Verification
Type
grant
Keywords

Finite on automata on finite and infinite objects, heuristics for efficient operations with automata, decision procedures, formal analysis and verification, shape analysis, string analysis, termination and liveness analysis.

Abstract

As indicated already above, the essence of the project is to deliver a strong push towards unleashing the potential of automata in practice through efficient heuristics. The efficiency of the heuristics should be demonstrated by using the developed techniques to advance the state of the art in shape analysis, string analysis, and termination/liveness analysis.

Team members
Holík Lukáš, doc. Mgr., Ph.D. (DITS FIT BUT) , research leader
Strejček Jan, prof. RNDr., Ph.D. (FI MUNI) , team leader
Andriushchenko Roman, Ing. (DITS FIT BUT)
Češka Milan, doc. RNDr., Ph.D. (DITS FIT BUT)
Havlena Vojtěch, Ing., Ph.D. (DITS FIT BUT)
Holíková Lenka, Ing. (DITS FIT BUT)
Hošták Viliam Samuel, Ing. (FIT BUT)
Hruška Martin, Ing. (DITS FIT BUT)
Chocholatý David, Ing. (FIT BUT)
Janků Petr, Ing. (DITS FIT BUT)
Křivka Zbyněk, Ing., Ph.D. (DIFS FIT BUT)
Lengál Ondřej, Ing., Ph.D. (DITS FIT BUT)
Malásková Věra (DITS FIT BUT)
Matyáš Jiří, Ing. (DITS FIT BUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (DITS FIT BUT)
Slezáková Alexandra, Bc. (FIT BUT)
Šedý Michal, Ing. (FIT BUT)
Šoková Veronika, Ing. (DITS FIT BUT)
Turcel Matej, Ing. (FIT BUT)
Vargovčík Pavol, Ing. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Publications

2023

  • HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions. Journal of Systems and Software, vol. 201, no. 201, 2023, pp. 111673-111693. ISSN 0164-1212. Detail
  • HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej and TURRINI Andrea. A symbolic algorithm for the case-split rule in solving word constraints with extensions (technical report). Ithaca: Cornell University Library, 2023. Detail

2021

  • HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej and VOJNAR Tomáš. Automata Terms in a Lazy WSkS Decision Procedure. Journal of Automated Reasoning, vol. 65, no. 7, 2021, pp. 971-999. ISSN 0168-7433. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej and ŠMAHLÍKOVÁ Barbora. Deciding S1S: Down the Rabbit Hole and Through the Looking Glass. In: Proceedings of NETYS'21. Lecture notes in Computer Science. Cham: Springer Verlag, 2021, pp. 215-222. ISSN 0302-9743. Detail
  • KÖVÁRI Adam, KŘIVKA Zbyněk and MEDUNA Alexander. Evaluating Yona Language. In: INTERNATIONAL CONFERENCES ON WWW/INTERNET 2021 AND APPLIED COMPUTING 2021. Lisabon: International Association for Development of the Information Society, 2021, pp. 101-108. ISBN 978-989-8704-34-4. Detail
  • HOLÍK Lukáš and VARGOVČÍK Pavol. Simplifying Alternating Automata for Emptiness Testing. In: Programming Languages and Systems - 19th Asian Symposium, APLAS 2021, Chicago, IL, USA, October 17-18, 2021, Proceedings. Cham: Springer International Publishing, 2021, pp. 243-264. ISBN 978-3-030-89051-3. Detail
  • HOLÍK Lukáš and HRUŠKA Martin. Towards Efficient Shape Analysis with Tree Automata. In: Proceedings International Conference on Networked Systems. Lecture notes in Computer Science. Cham: Springer Verlag, 2021, pp. 206-214. ISSN 0302-9743. Detail

2020

  • MATYÁŠ Jiří, PANKUCH Adam, VOJNAR Tomáš, ČEŠKA Milan and ČEŠKA Milan. Approximating Complex Arithmetic Circuits with Guaranteed Worst-Case Relative Error. In: International Conference on Computer Aided Systems Theory (EUROCAST'19). Lecture Notes in Computer Science, vol. 12013. Cham: Springer Verlag, 2020, pp. 482-490. ISBN 978-3-030-45092-2. Detail

2019

  • ČEŠKA Milan, HENSE Christian, JUNGES Sebastian and KATOEN Joost-Pieter. Counterexample-Driven Synthesis for Probabilistic Program Sketches. In: Proceedings of the 23rd International Symposium on Formal Methods.. Lecture Notes of Computer Science. Porto: Springer International Publishing, 2019, pp. 101-120. ISBN 978-3-030-30941-1. Detail
  • ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš and JANKŮ Petr. Chain-Free String Constraints. In: Proceedings of ATVA'19. Lecture Notes in Computer Science, vol. 11781. Cham: Springer International Publishing, 2019, pp. 277-293. ISBN 978-3-030-31783-6. Detail
  • ČEŠKA Milan, HENSE Christian, JANSEN Nils, JUNGES Sebastian and KATOEN Joost-Pieter. Model Repair Revamped - On the Automated Synthesis of Markov Chains -. From Reactive Systems to Cyber-Physical Systems. Lecture Notes of Computer Science. Cham: Springer International Publishing, 2019, pp. 107-125. ISBN 978-3-030-31513-9. Detail
  • ČEŠKA Milan and KŘETÍNSKÝ Jan. Semi-Quantitative Abstraction and Analysis of Chemical Reaction Networks. In: Proceedings of the 31th International Conference on Computer Aided Verification (CAV'19). Lecture Notes of Computer Science, vol. 11561. New York: Springer International Publishing, 2019, pp. 475-496. ISBN 978-3-030-25540-4. Detail
  • ČEŠKA Milan and KŘETÍNSKÝ Jan. Semi-quantitative Abstraction and Analysis of Chemical Reaction Networks (Extended Abstract). In: Proceedings of the 17th International Conference on Computational Methods in Systems Biology. Lecture Notes in Bioinformatics. Trieste: Springer International Publishing, 2019, pp. 337-341. ISBN 978-3-030-31303-6. Detail
  • CHEN Yu-Fang, HAVLENA Vojtěch and LENGÁL Ondřej. Simulations in Rank-Based Büchi Automata Complementation. In: Proceedings of 17th Asian Symposium on Programming Languages and Systems (APLAS). Nusa Dua: Springer International Publishing, 2019, pp. 447-467. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, HOLÍKOVÁ Lenka, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus and VOJNAR Tomáš. Succinct Determinisation of Counting Automata via Sphere Construction. In: In Proc. of 17th Asian Symposium on Programming Languages and Systems - APLAS'19. Berlin Heidelberg: Springer Verlag, 2019, pp. 468-489. ISSN 0302-9743. Detail
  • HOLÍK Lukáš, HOLÍKOVÁ Lenka, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus and VOJNAR Tomáš. Succinct Determinisation of Counting Automata via Sphere Construction (Technical Report). Ithaca: Cornell University Library, 2019. Detail
Products

2019

  • Trau: SMT solver for string constraints, software, 2019
    Authors: Abdulla Parosh A., Atig Mohamed F., Bui Phi Diep, Holík Lukáš, Chen Yu-Fang, Rezine Ahmed, Rummer Philipp Detail

2015

  • Norn: An SMT Solver for String Constraints, software, 2015
    Authors: Abdulla Parosh A., Atig Mohamed F., Holík Lukáš, Chen Yu-Fang, Rezine Ahmed, Stenman Jari Detail
Back to top