Detail projektu

Scalable Techniques for Analysis of Complex Properties of Computer Systems

Období řešení: 1. 1. 2020 – 31. 12. 2022

Typ projektu: grant

Kód: GA20-07487S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název česky
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů
Typ
grant
Klíčová slova

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.

Abstrakt

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.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS) – hlavní řešitel
Gaďorek Petr, Ing. (DFIT-OIP)
Harmim Dominik, Ing.
Holík Lukáš, doc. Mgr., Ph.D. (UITS)
Kofroň Jan, doc. RNDr., Ph.D.
Lengál Ondřej, Ing., Ph.D. (UITS)
Mrazíková Libuše, Mgr. (DFIT-PO)
Oravcová Marcela, Ing. (DFIT-EO)
Paulíková Barbora, Mgr. (DFIT-PO)
Pirová Zuzana, Ing. (DFIT-EO)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS)
Štanclová Eva (DFIT-EO)
Ventrubová Hana (DFIT-EO)
Publikace

2023

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

2022

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

2021

  • 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
  • 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
  • CHALUPA, M.; JAŠEK, T.; ŘECHTÁČKOVÁ, A.; STREJČEK, J.; ŠOKOVÁ, V.; NOVÁK, J. Symbiotic 8: Beyond Symbolic Execution. 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

2020

  • 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
  • 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
  • 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
Nahoru