Detail projektu

SNAPPY - 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 FIT VUT) , hlavní řešitel
Kofroň Jan, doc. RNDr., Ph.D. (MFF UK) , spoluřešitel
Gaďorek Petr, Ing. (CVT FIT VUT)
Harmim Dominik, Ing. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Mrazíková Libuše, Mgr. (Děkanát FIT VUT)
Oravcová Marcela, Ing. (Děkanát FIT VUT)
Paulíková Barbora, Mgr. (Děkanát FIT VUT)
Pirová Zuzana, Ing. (Děkanát FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)
Štanclová Eva (Děkanát FIT VUT)
Ventrubová Hana (Děkanát FIT VUT)
Publikace

2023

  • FIEDOR Jan, KŘENA Bohuslav, SMRČKA Aleš, VAŠÍČEK Ondřej a VOJNAR Tomáš. Integrating OSLC Services into Eclipse. In: Computer Aided Systems Theory - EUROCAST 2022. Lecture Notes in Computer Science, roč. 13789. Las Palmas de Gran Canaria: Springer International Publishing, 2023, s. 240-249. ISBN 978-3-031-25311-9. Detail
  • FIEDOR Tomáš, HRUŠKA Martin a SMRČKA Aleš. Orchestrating Digital Twins for Distributed Manufacturing Execution Systems. In: Computer Aided Systems Theory - EUROCAST 2022. Lecture Notes in Computer Science, roč. 13789. Zurich: Springer International Publishing, 2023, s. 223-231. ISBN 978-3-031-25311-9. Detail
  • HARMIM Dominik, MARCIN Vladimír, SVOBODOVÁ Lucie a VOJNAR Tomáš. Static Deadlock Detection in Low-Level C Code. In: International Conference on Computer Aided Systems Theory (EUROCAST'22). Lecture Notes in Computer Science, roč. 13789. Cham: Springer Nature Switzerland AG, 2023, s. 267-276. ISBN 978-3-031-25311-9. Detail
  • BLAHOUDEK František, HAVLENA Vojtěch, HOLÍK Lukáš, CHEN Yu-Fang, CHOCHOLATÝ David, LENGÁL Ondřej a SÍČ Juraj. Word Equations in Synergy with Regular Constraints. In: Proceedings of FM'23. Lübeck: Springer Verlag, 2023, s. 403-423. ISSN 0302-9743. Detail

2022

  • MALÍK Viktor, ŠILLING Petr a VOJNAR Tomáš. Applying Custom Patterns in Semantic Equality Analysis. In: Networked Systems. Lecture Notes in Computer Science, roč. 13464. Cham: Springer Nature Switzerland AG, 2022, s. 265-282. ISBN 978-3-031-17436-0. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej a ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker. In: Proceedings of the 34th International Conference on Computer Aided Verification. Haifa: Springer Verlag, 2022, s. 188-201. ISBN 978-3-031-13187-5. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej a ŠMAHLÍKOVÁ Barbora. Complementing Büchi Automata with Ranker (Technical Report). Ithaca: Cornell University Library, 2022. Detail
  • HOLÍKOVÁ Lenka, HOLÍK Lukáš, HOMOLIAK Ivan, LENGÁL Ondřej, VEANES Margus a VOJNAR Tomáš. Counting in Regexes Considered Harmful: Exposing ReDoS Vulnerability of Nonbacktracking Matchers. In: Proceedings of the 31st USENIX Security Symposium. Boston, MA: USENIX, 2022, s. 4165-4182. ISBN 978-1-939133-31-1. Detail
  • HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš a ZULEGER Florian. Low-Level Bi-Abduction. In: 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics, roč. 2022. Wadern: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2022, s. 1-30. ISBN 978-3-95977-225-9. ISSN 1868-8969. Detail
  • HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš a ZULEGER Florian. Low-Level Bi-Abduction (Artifact). Dagstuhl, 2022. Detail
  • HOLÍK Lukáš, PERINGER Petr, ROGALEWICZ Adam, ŠOKOVÁ Veronika, VOJNAR Tomáš a ZULEGER Florian. Low-Level Bi-Abduction (technical report). Ithaca, 2022. Detail
  • FIEDOR Tomáš, PAVELA Jiří, ROGALEWICZ Adam a VOJNAR Tomáš. 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, s. 499-503. ISBN 978-1-6654-7956-1. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej a ŠMAHLÍKOVÁ Barbora. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation. In: Proceedings of TACAS'22. Munich: Springer Verlag, 2022, s. 118-136. ISBN 978-3-030-99526-3. ISSN 0302-9743. Detail
  • HAVLENA Vojtěch, LENGÁL Ondřej a ŠMAHLÍKOVÁ Barbora. Sky Is Not the Limit: Tighter Rank Bounds for Elevator Automata in Buchi Automata Complementation (Technical Report). Ithaca, 2022. Detail
  • VAŠÍČEK Ondřej, FIEDOR Jan, KRATOCHVÍLA Tomáš, KŘENA Bohuslav, SMRČKA Aleš a VOJNAR Tomáš. 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, s. 1408-1418. ISBN 978-1-4503-9413-0. Detail
  • CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Utilizing parametric systems for detection of pipeline hazards. International Journal on Software Tools for Technology Transfer, roč. 2020, č. 1, 2022, s. 1-28. ISSN 1433-2779. Detail

2021

  • MALÍK Viktor a VOJNAR Tomáš. 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, s. 329-339. ISBN 978-1-7281-6837-1. Detail
  • HAVLENA Vojtěch a LENGÁL Ondřej. Reducing (to) the Ranks: Efficient Rank-based Büchi Automata Complementation. In: 32nd International Conference on Concurrency Theory (CONCUR 2021). Paris: Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2021, s. 1-19. ISSN 1868-8969. Detail
  • CHALUPA Marek, JAŠEK Tomáš, NOVÁK Jakub, ŘECHTÁČKOVÁ Anna, STREJČEK Jan a ŠOKOVÁ Veronika. Symbiotic 8: Beyond Symbolic Execution. In: Proceedings of TACAS 2021 (2). Lecture Notes in Computer Science, roč. 12652. Cham: Springer International Publishing, 2021, s. 453-457. ISBN 978-3-030-72012-4. Detail
  • HOMOLIAK Ivan, VENUGOPALAN Sarad, REIJSBERGEN Daniel, HUM Qingze, SCHUMI Richard a SZALACHOWSKI Pawel. The Security Reference Architecture for Blockchains: Toward a Standardized Model for Studying Vulnerabilities, Threats, and Defenses. IEEE Communications Surveys and Tutorials, roč. 23, č. 1, 2021, s. 341-390. ISSN 1553-877X. Detail

2020

  • MALÍK Viktor, SCHRAMMEL Peter a VOJNAR Tomáš. 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, roč. 12079. Dublin: Springer International Publishing, 2020, s. 368-372. ISBN 978-3-030-45236-0. Detail
  • 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
  • HUM Qingze, TAN Wei Jin, TEY Shi Ying, LENUS Latasha, HOMOLIAK Ivan, LIN Yun a SUN Jun. 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, s. 17-25. ISBN 978-0-7381-0495-9. Detail
Produkty

2023

  • DiffKemp: Statický analyzátor sémantických rozdílů, verze 0.4.0, software, 2023
    Autoři: Glozar Tomáš, Malecová Tatiana, Malík Viktor, Rozek Jakub, Šilling Petr, Vojnar Tomáš, Žáčik Pavol 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
  • GadgetCA - Nástroj pro generování ReDoS útoků, software, 2022
    Autoři: Holík Lukáš, Holíková Lenka, Homoliak Ivan, Lengál Ondřej, Veanes Margus, Vojnar Tomáš Detail
  • Ranker: Nástroj pro komplementaci Büchiho automatů, software, 2022
    Autoři: Havlena Vojtěch, Lengál Ondřej, Šmahlíková Barbora Detail
  • Unite: Adaptér pro zpřístupnění nástrojů pro analýzu softwaru přes webové služby s využitím OSLC, Verze 3.0, software, 2022
    Autoři: Vašíček Ondřej, Fiedor Jan, Smrčka Aleš, Vojnar Tomáš, Křena Bohuslav Detail
Nahoru