The overall goal of the project is to significantly improve state-of-the-art techniques of automated analysis and verification to make them more scalable on one hand and applicable for handling more complex properties of more complex code on the other hand. For that, a set of mutually complementary analyses handling complex data and control structures, identified above as problematic for current analyses, will be proposed, covering particular goals form the following areas: (1) pointer programs, (2) string and array programs, and (3) concurrent programs.

Description in Czech
Obecným cílem projektu je výrazně zlepšit současné techniky automatizované analýzy a verifikace tak, aby lépe škálovaly a mohly být aplikovány pro analýzu složitějších vlastností pokročilejších programů. Konkrétně se projekt zaměří na programy s (1) ukazateli, (2) řetězci a poli a (3) paralelismy.

Keywords
Automated analysis and verification, static analysis, formal methods, dynamic analysis, pointers and dynamic data structures, arrays and strings, concurrency.

Key words in Czech
Automatická analýza a verifikace programů, statická analýza, formální metody, dynamická analýza, ukazatele a dynamické datové struktury, pole a řetězce, paralelismus.

GA20-07487S

English

Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsible
Holík Lukáš, doc. Mgr., Ph.D. - fellow researcher
Lengál Ondřej, Ing., Ph.D. - fellow researcher
Rogalewicz Adam, doc. Mgr., Ph.D. - fellow researcher

Department of Intelligent Systems
- responsible department (3.4.2019 - 31.12.2022)
Department of Intelligent Systems
- beneficiary (3.4.2019 - 31.12.2022)

HARMIM, D.; MARCIN, V.; SVOBODOVÁ, L.; VOJNAR, T. Static Deadlock Detection in Low-Level C Code. In International Conference on Computer Aided Systems Theory (EUROCAST'22). Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2023. p. 267-276. ISBN: 978-3-031-25311-9.
Detail

HRUŠKA, M.; FIEDOR, T.; SMRČKA, A. Orchestrating Digital Twins for Distributed Manufacturing Execution Systems. In Computer Aided Systems Theory - EUROCAST 2022. Lecture Notes in Computer Science. Zurich: Springer International Publishing, 2023. p. 223-231. ISBN: 978-3-031-25311-9.
Detail

HAVLENA, V.; CHOCHOLATÝ, D.; LENGÁL, O.; HOLÍK, L.; SÍČ, J.; BLAHOUDEK, F.; CHEN, Y. Word Equations in Synergy with Regular Constraints. In Proceedings of FM'23. Lecture Notes in Computer Science. Lübeck: Springer Verlag, 2023. p. 403-423. ISSN: 0302-9743.
Detail

FIEDOR, J.; KŘENA, B.; SMRČKA, A.; VAŠÍČEK, O.; VOJNAR, T. Integrating OSLC Services into Eclipse. In Computer Aided Systems Theory - EUROCAST 2022. Lecture Notes in Computer Science. Las Palmas de Gran Canaria: Springer International Publishing, 2023. p. 240-249. ISBN: 978-3-031-25311-9.
Detail

MALÍK, V.; GLOZAR, T.; VOJNAR, T.; ŠILLING, P.; ŽÁČIK, P.; MALECOVÁ, T.; ROZEK, J.: DiffKemp 0.4.0; DiffKemp: Static Analyser of Semantic Differences, version 0.4.0. https://github.com/viktormalik/diffkemp/releases/tag/v0.4.0. URL: https://github.com/viktormalik/diffkemp/releases/tag/v0.4.0. (software)
Detail

VAŠÍČEK, O.; FIEDOR, J.; KRATOCHVÍLA, T.; KŘENA, B.; SMRČKA, A.; VOJNAR, T. Unite: An Adapter for Transforming Analysis Tools to Web Services via OSLC. In ESEC/FSE 2022: Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering. Singapore: Association for Computing Machinery, 2022. p. 1408-1418. ISBN: 978-1-4503-9413-0.
Detail

ŠILLING, P.; MALÍK, V.; VOJNAR, T. Applying Custom Patterns in Semantic Equality Analysis. In Networked Systems. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2022. p. 265-282. ISBN: 978-3-031-17436-0.
Detail

FIEDOR, T.; PAVELA, J.; ROGALEWICZ, A.; VOJNAR, T. Perun: Performance Version System. In Proceedings of the 38th IEEE International Conference on Software Maintenance and Evolution (ICSME 2022). Limassol: Institute of Electrical and Electronics Engineers, 2022. p. 499-503. ISBN: 978-1-6654-7956-1.
Detail

VAŠÍČEK, O.; FIEDOR, J.; SMRČKA, A.; VOJNAR, T.; KŘENA, B.: Unite 3.0; Unite: An Adapter for Transforming Analysis Tools to Web Services via OSLC, Version 3.0. https://pajda.fit.vutbr.cz/verifit/unite/-/tags/v3.0.0. URL: https://pajda.fit.vutbr.cz/verifit/unite/-/tags/v3.0.0. (software)
Detail

HOLÍK, L.; HOLÍKOVÁ, L.; HOMOLIAK, I.; LENGÁL, O.; VOJNAR, T.; VEANES, M.: gadgetca; GadgetCA: A Tool for Generating ReDoS Attacks. Nástroj i dokumentaci lze získat na URL: http://www.fit.vutbr.cz/research/groups/verifit/tools/gadgetca. URL: https://www.fit.vut.cz/research/product/730/. (software)
Detail

HOLÍK, L.; PERINGER, P.; ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; ZULEGER, F. Low-Level Bi-Abduction (technical report). Ithaca: 2022. p. 0-0.
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022. p. 0-0.
Detail

ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F. Low-Level Bi-Abduction (Artifact). Dagstuhl: 2022. p. 1-6.
Detail

HOLÍK, L.; PERINGER, P.; ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; ZULEGER, F. Low-Level Bi-Abduction. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics, LIPIcs. Leibniz International Proceedings in Informatics. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2022. p. 1-30. ISBN: 978-3-95977-225-9. ISSN: 1868-8969.
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Complementing Büchi Automata with Ranker. In Proceedings of the 34th International Conference on Computer Aided Verification. Lecture Notes in Computer Science. Haifa: Springer Verlag, 2022. p. 188-201. ISBN: 978-3-031-13187-5. ISSN: 0302-9743.
Detail

HOLÍKOVÁ, L.; HOLÍK, L.; HOMOLIAK, I.; LENGÁL, O.; VEANES, M.; VOJNAR, T. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In Proceedings of the 31st USENIX Security Symposium. Boston, MA: USENIX, 2022. p. 4165-4182. ISBN: 978-1-939133-31-1.
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B.: Ranker; Ranker: A Tool for Complementing Büchi Automata. https://github.com/vhavlena/ranker. URL: https://github.com/vhavlena/ranker. (software)
Detail

ROGALEWICZ, A.; ŠOKOVÁ, V.; VOJNAR, T.; HOLÍK, L.; PERINGER, P.; ZULEGER, F.: broom; Broom: A Static Analyzer for C Based on Separation Logic and the Principle of Bi-Abductive Reasoning. https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1. URL: https://pajda.fit.vutbr.cz/rogalew/broom/-/tree/v0.0.1. (software)
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation (Technical Report). Ithaca: 2022. p. 0-0.
Detail

HAVLENA, V.; LENGÁL, O.; ŠMAHLÍKOVÁ, B. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation. In Proceedings of TACAS'22. Lecture Notes in Computer Science. Munich: Springer Verlag, 2022. p. 118-136. ISBN: 978-3-030-99526-3. ISSN: 0302-9743.
Detail

Responsibility: Vojnar Tomáš, prof. Ing., Ph.D.