Automata for Decision Procedures and Verification (AUTODEV)
- Kód projektu
- GA19-24397S
- Období řešení
- 1/2019 - 12/2021
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Standardní projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Spolupracující organizace
-
Vysoké učení technické v Brně
- Odpovědná osoba 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.
Publikace
Počet publikací: 5
2020
-
LTL to self-loop alternating automata with generic acceptance and back
Theoretical Computer Science, rok: 2020, ročník: Neuveden, vydání: 840, 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, rok: 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, rok: 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, rok: 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, rok: 2019