Detail projektu
Efektivní konečné automaty pro automatické usuzování
Období řešení: 1. 1. 2020 - 31. 12. 2024
Typ projektu: grant
Kód: LL1908
Agentura: Ministerstvo školství, mládeže a tělovýchovy České republiky
Program: ERC CZ
konečné automaty, logika, automatizované uvažování, formální verifikace, analýza programu, analýza tvaru, analýza řetězcových programů, bezpečnost
Cílem projektu je zlepšit efektivitu základních technik konečných automatů. Konečný automat je základní koncepcí informatiky s četnými aplikacemi. Výzkum automatů přináší neustále nové výsledky týkající se široké škály aplikací v automatizovaném rozhodování, formálním ověřování, zpracování jazyka, databázích a webových technologiích. Bohužel jejich praktický dopad, i když je pozoruhodný, je do značné míry omezen nedostatečnou škálovatelností automatických technik zakořeněné ve velmi základních pojmech a algoritmech. Efektivnost automatické technologie však není dostatečně vyřešena. Výzkum se většinou zaměřuje na různá rozšíření automatů a vzrušující "teoretické" aplikace. Důvodem této nedostatečné pozornosti je skutečnost, že se základní automatizační techniky zdají být z obvyklé automatické teoretické perspektivy již dobře pochopené, a proto neposkytují dostatek prostoru pro výzkum. Je zapotřebí vyvinout soustředěné úsilí a přijít s novými myšlenkami v mnohem pragmatickějším směru, abych mohlo dojít k posunutí vývoje. Příležitost v dosažení průlomu v efektivnosti rozhodování vidím ve využití automatů, které vychází z pokroku v automatizovaném rozhodování a ověřování. Koncepty, jako je líné hodnocení, symbolické reprezentace, abstrakce nebo heuristika z řešení SAT / SMT, lze kombinovat s tradičními automatovými technikami a zpracovat novým způsobem. Plánuji detailně prozkoumat základní automatové nástroje společně s těmito koncepty s důrazem na jejich výkonnost v praxi. Jsem přesvědčen, že když výkonnost v praxi získává zaslouženou pozornost, můžeme očekávat podobně rychlý pokrok, jaký byl např. u řešení problému SAT / SMT nebo u ověřování softwaru, což může vést k velmi užitečným a prakticky škálovatelným metodám a nástrojům, stejně jako k novým příležitostem pro hluboké teoretické studium nových technik.
Blahoudek František, RNDr., Ph.D. (UITS FIT VUT)
Češka Milan, doc. RNDr., Ph.D. (UITS FIT VUT)
Fiedor Tomáš, Ing., Ph.D. (UITS FIT VUT)
Havlena Vojtěch, Ing., Ph.D. (UITS FIT VUT)
Homoliak Ivan, Ing., Ph.D. (UITS FIT VUT)
Horký Michal, Ing. (FIT VUT)
Hošták Viliam Samuel, Ing. (FIT VUT)
Kesiraju Michaela, Bc. (FIT VUT)
Křivka Zbyněk, Ing., Ph.D. (UIFS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Martiček Štefan, Ing. (UITS FIT VUT)
Meduna Alexander, prof. RNDr., CSc. (UIFS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Síč Juraj, Mgr. (UITS FIT VUT)
Slezáková Alexandra, Bc. (FIT VUT)
Šedý Michal, Bc. (FIT VUT)
Šoková Veronika, Ing. (UITS FIT VUT)
Toth Vaňo Pavol (FIT VUT)
Turoňová Lenka, Ing. (UITS FIT VUT)
2021
- SÍČ Juraj a STREJČEK Jan. DQBDD: An Efficient BDD-Based DQBF Solver. In: Proc. of the 24th International Conference on Theory and Applications of Satisfiability Testing. Heidelberg: Springer Verlag, 2021, s. 535-544. ISSN 0302-9743. Detail
- MATOUŠEK Petr, HAVLENA Vojtěch a HOLÍK Lukáš. Efficient Modelling of ICS Communication For Anomaly Detection Using Probabilistic Automata. In: Proceedings of IFIP/IEEE International Symposium on Integrated Network Management. Bordeaux: International Federation for Information Processing, 2021, s. 81-89. ISBN 978-3-903176-32-4. Detail
- KŘIVKA Zbyněk a MEDUNA Alexander. Scattered Context Grammars with One Non-Context-Free Production are Computationally Complete. Fundamenta Informaticae, roč. 179, č. 4, 2021, s. 361-384. ISSN 0169-2968. Detail
2020
- HAVLENA Vojtěch, CHEN Yu-Fang, LENGÁL Ondřej a TURRINI Andrea. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In: Proceedings of APLAS'20. Heidelberg: Springer Verlag, 2020, s. 343-363. ISSN 0302-9743. Detail
- HAVLENA Vojtěch, HOLÍK Lukáš, LENGÁL Ondřej, VALEŠ Ondřej a VOJNAR Tomáš. Antiprenexing for WSkS: A Little Goes a Long Way. In: EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020, s. 298-316. ISSN 2398-7340. Detail
- ABDULLA Parosh A., ATIG Mohamed F., BUI Phi Diep, HOLÍK Lukáš, CHEN Yu-Fang, JANKŮ Petr, LIN Hsin-Hung a WU Wei-Cheng. Efficient handling of string-number conversion. In: Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). New York: Association for Computing Machinery, 2020, s. 943-957. ISBN 978-1-4503-7613-6. Detail
- HOLÍK Lukáš, LENGÁL Ondřej, SAARIKIVI Olli, VEANES Margus, VOJNAR Tomáš a TUROŇOVÁ Lenka. Regex Matching with Counting-Set Automata. Proceedings of the ACM on Programming Languages, roč. 4, č. 11, 2020, s. 1-30. ISSN 2475-1421. Detail
2022
- Broom: Nástroj pro statickou analýzu C programů založen na separační logice a bi-abdukčním přístupu, software, 2022
Autoři: Holík Lukáš, Peringer Petr, Rogalewicz Adam, Šoková Veronika, Vojnar Tomáš, Zuleger Florian Detail
2020
- Chipmunk: Nástroj slouží k hledání vzorů pomocí čítačových automatů s registry., software, 2020
Autoři: Holík Lukáš, Lengál Ondřej, Turoňová Lenka, Veanes Margus, Vojnar Tomáš Detail