Project detail

Scalable Techniques for Analysis of Complex Properties of Computer Systems

Duration: 01.01.2020 — 31.12.2022

Funding resources

Czech Science Foundation - Standardní projekty

- part funder (2020-01-01 - 2022-12-31)

On the project

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.

Mark

GA20-07487S

Default language

English

People 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
Vojnar Tomáš, prof. Ing., Ph.D. - principal person responsible

Units

Department of Intelligent Systems
- beneficiary (2019-04-03 - 2022-12-31)

Results

MALÍK, V.; SCHRAMMEL, P.; VOJNAR, T. 2LS: Heap Analysis and Memory Safety (Competition Contribution). In Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2. Lecture Notes in Computer Science. Dublin: Springer International Publishing, 2020. p. 368-372. ISBN: 978-3-030-45236-0.
Detail

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

HAVLENA, V.; LENGÁL, O.; CHEN, Y.; TURRINI, A. A Symbolic Algorithm for the Case-Split Rule in String Constraint Solving. In Proceedings of APLAS'20. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2020. p. 343-363. ISSN: 0302-9743.
Detail

HUM, Q.; TAN, W.; TEY, S.; LENUS, L.; HOMOLIAK, I.; LIN, Y.; SUN, J. CoinWatch: A Clone-Based Approach for Detecting Vulnerabilities in Cryptocurrencies. In 3rd IEEE INTERNATIONAL CONFERENCE ON BLOCKCHAIN (BLOCKCHAIN 2020). Rhodos: Institute of Electrical and Electronics Engineers, 2020. p. 17-25. ISBN: 978-0-7381-0495-9.
Detail

HOMOLIAK, I.; VENUGOPALAN, S.; REIJSBERGEN, D.; HUM, Q.; SCHUMI, R.; SZALACHOWSKI, P. The Security Reference Architecture for Blockchains: Toward a Standardized Model for Studying Vulnerabilities, Threats, and Defenses. IEEE COMMUN SURV TUT, 2021, vol. 23, no. 1, p. 341-390. ISSN: 1553-877X.
Detail

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Utilizing parametric systems for detection of pipeline hazards. International Journal on Software Tools for Technology Transfer, 2022, vol. 2020, no. 1, p. 1-28. ISSN: 1433-2779.
Detail

CHALUPA, M.; JAŠEK, T.; ŘECHTÁČKOVÁ, A.; STREJČEK, J.; ŠOKOVÁ, V.; NOVÁK, J. Symbiotic 8: Beyond Symbolic Execution (Competition Contribution). In Proceedings of TACAS 2021 (2). Lecture Notes in Computer Science. Cham: Springer International Publishing, 2021. p. 453-457. ISBN: 978-3-030-72012-4.
Detail

MALÍK, V.; VOJNAR, T. Automatically Checking Semantic Equivalence between Versions of Large-Scale C Projects. In 2021 14th IEEE Conference on Software Testing, Verification and Validation (ICST). Porto de Galinhas: Institute of Electrical and Electronics Engineers, 2021. p. 329-339. ISBN: 978-1-7281-6837-1.
Detail

HAVLENA, V.; LENGÁL, O. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics, LIPIcs. Paris: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021. p. 1-19. ISSN: 1868-8969.
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

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.; HOLÍK, L.; LENGÁL, O.; VALEŠ, O.; VOJNAR, T. Antiprenexing for WSkS: A Little Goes a Long Way. In EPiC Series in Computing. Proceedings of LPAR-23. Manchester: EasyChair, 2020. p. 298-316. ISSN: 2398-7340.
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

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

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. 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Í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

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

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

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

Š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

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.; 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

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

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