Project information
Automata for Decision Procedures and Verification
(AUTODEV)
- Project Identification
- GA19-24397S
- Project Period
- 1/2019 - 12/2021
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
- Cooperating Organization
-
Brno University of Technology
- Responsible person doc. Mgr. Lukáš Holík, Ph.D.
Výzkum konečných automatů je tradiční disciplínou, která dlouhodobě produkuje množství výsledků potenciálně využitelných v mnoha oblastech, jako jsou verifikace, zpracování přirozeného jazyka, databáze, nebo webové technologie. Praktická využitelnost těchto výsledků je však limitována nedostatečnou škálovatelností automatové technologie. Protože příčiny této neefektivity tkví v nejzákladnějších technikách a konceptech automatové technologie, potřebný pokrok v této oblasti vyžaduje výrazně nové a přístupy k řešení klasických problémů. V tomto projektu navrhujeme hledat cestu k novým řešením skrze kombinaci tradiční automatové technologie s technikami úspěšnými ve verifikaci a automatickém usuzování, jako jsou líné vyhodnocování, symbolická reprezentace, abstrakce, a techniky SAT/SMT-solvingu. Sílu nových automatových metod pak budeme demonstrovat na několika konkrétních aplikačních doménách: na analýze ukazatelových programů, programů manipulujících řetězce, a na analýze zdrojů a terminace.
Publications
Total number of publications: 7
2022
-
Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding
Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, year: 2022
-
Symbiotic-Witch: A Klee-Based Violation Witness Checker
Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, year: 2022
2020
-
LTL to self-loop alternating automata with generic acceptance and back
Theoretical Computer Science, year: 2020, volume: 840, edition: Nov 2020, DOI
-
Seminator 2 Can Complement Generalized Büchi Automata via Improved Semi-determinization
Computer Aided Verification - 32nd International Conference, CAV 2020, Los Angeles, CA, USA, July 21-24, 2020, Proceedings, Part II, year: 2020
2019
-
Generic Emptiness Check for Fun and Profit
Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, year: 2019
-
LTL to Smaller Self-Loop Alternating Automata and Back
Theoretical Aspects of Computing - ICTAC 2019 - 16th International Colloquium, Hammamet, Tunisia, October 31 - November 4, 2019, Proceedings, year: 2019
-
ltl3tela: LTL to Small Deterministic or Nondeterministic Emerson-Lei Automata
Automated Technology for Verification and Analysis - 17th International Symposium, ATVA 2019, Taipei, Taiwan, October 28-31, 2019, Proceedings, year: 2019