Informace o projektu
Pokročilá analýza a verifikace pro pokročilý software
(AIDE)
- Kód projektu
- GA23-06506S
- Období řešení
- 1/2023 - 12/2025
- Investor / Programový rámec / typ projektu
-
Grantová agentura ČR
- Standardní projekty
- Fakulta / Pracoviště MU
- Fakulta informatiky
- Spolupracující organizace
-
Univerzita Karlova v Praze
- Odpovědná osoba doc. RNDr. Jan Kofroň, Ph.D.
- Odpovědná osoba prof. Ing. Tomáš Vojnar, Ph.D.
S cílem pomoci vývojářům software vyrovnat se s jeho obrovskou a stále rostoucí složitostí se projekt zaměřuje na nové metody automatizované analýzy a verifikace pokročilého software, založeného na nízkoúrovňovém programování, moderních vysokoúrovňových přístupech či obojím. Projekt bude rozvíjet zejména metody založené na logice, jako je bi-abduktivní analýza nebo symbolické provádění, vhodně kombinované s přístupy, jako je abstraktní interpretace, „slicing“ či pokročilé typové systémy. Pro zefektivnění uvažovaných metod založených na logice budou rovněž vyvíjeny rozhodovací procedury pro různé uvažované logiky (např. separační logiku, kvantifikovanou bit-vektorovou logiku či Hornovy klauzule s omezeními). Mezi nízkoúrovňové programy, jež jsou cílem vyvíjených verifikačních metod, patří zejména programy využívající nízkoúrovňovou manipulaci s ukazateli a dynamickými datovými strukturami, zatímco mezi uvažované vysokoúrovňové programy patří programy založené na expertních systémech, vysokoúrovňové specifikace software či programy v moderních vysokoúrovňových jazycích, jako je Scala.
Cíle udržitelného rozvoje
Masarykova univerzita se hlásí k cílům udržitelného rozvoje OSN, jejichž záměrem je do roku 2030 zlepšit podmínky a kvalitu života na naší planetě.
Publikace
Počet publikací: 6
2024
-
Fizzer: New Gray-Box Fuzzer
Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, rok: 2024
-
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, rok: 2024
-
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, rok: 2024
-
Tighter Construction of Tight Büchi Automata
Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, rok: 2024
-
Witch 3: Validation of Violation Witnesses in the Witness Format 2.0
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, rok: 2024
2023
-
Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation
Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II, rok: 2023