Detail projektu
Pokročilá analýza a verifikace pro pokročilý software
Období řešení: 1. 1. 2023 – 31. 12. 2025
Typ projektu: grant
Kód: GA23-06506S
Agentura: Grantová agentura České republiky
Program: Standardní projekty
Název anglicky
Advanced Analysis and Verification for Advanced Software
Typ
grant
Klíčová slova
počítačové vědy, informatika, verifikace
Abstrakt
Dodat: Pokročilá analýza a verifikace pro pokročilý software
Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D.
(UITS)
– hlavní řešitel
Dacík Tomáš, Ing. (UITS)
Kofroň Jan, doc. RNDr., Ph.D.
Křena Bohuslav, Ing., Ph.D. (UITS)
Malásková Věra (UITS)
Michal Bohumil, Ing. (CVT)
Mrazíková Libuše, Mgr. (DFIT-PO)
Nesvedová Šárka (DFIT-PO)
Paulíčková Eva
Strejček Jan, prof. RNDr., Ph.D. (FIT)
Štanclová Eva (DFIT-EO)
Ventrubová Hana (DFIT-EO)
Dacík Tomáš, Ing. (UITS)
Kofroň Jan, doc. RNDr., Ph.D.
Křena Bohuslav, Ing., Ph.D. (UITS)
Malásková Věra (UITS)
Michal Bohumil, Ing. (CVT)
Mrazíková Libuše, Mgr. (DFIT-PO)
Nesvedová Šárka (DFIT-PO)
Paulíčková Eva
Strejček Jan, prof. RNDr., Ph.D. (FIT)
Štanclová Eva (DFIT-EO)
Ventrubová Hana (DFIT-EO)
Publikace
2024
- DACÍK, T.; ROGALEWICZ, A.; VOJNAR, T.; ZULEGER, F. Deciding Boolean Separation Logic via Small Models. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2024.
p. 188-206. ISBN: 978-3-031-57245-6. Detail - KOZÁK, D.; ČERNÝ, T.; ABDELFATTAH, A.; BLANCHARD, A.; HALE, J.; HUTCHESON, R.; LAMBARIA, N. Software Architecture Reconstruction for Microservice Systems using Static Analysis via GraalVM Native Image. In 2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER). Los Alamitos: Institute of Electrical and Electronics Engineers, 2024.
p. 12-22. ISBN: 979-8-3503-3066-3. Detail - KOZÁK, D.; STANCU, C.; WIMMER, C.; WÜRTHINGER, T. Scaling Type-Based Points-to Analysis with Saturation. Proceedings of the ACM on Programming Languages, 2024, vol. 8, no. PLDI,
p. 990-1013. ISSN: 2475-1421. Detail - MALÍK, V.; VOJNAR, T.; SCHRAMMEL, P. Template-Based Verification of Array-Manipulating Programs. In Taming the Infinities of Concurrency. Lecture Notes in Computer Science. Cham: Springer Nature Switzerland AG, 2024.
p. 206-224. ISBN: 978-3-031-56221-1. Detail - VAŠÍČEK, O.; ARIAS, J.; FIEDOR, J.; GUPTA, G.; HALL, B.; KŘENA, B.; LARSON, B.; VARANASI, S.; VOJNAR, T. Early Validation of High-Level System Requirements with Event Calculus and Answer Set Programming. Theory and Practice of Logic Programming, 2024, vol. 24, no. 4,
p. 844-862. ISSN: 1475-3081. Detail
2023
- HOLÍK, L.; HOLÍKOVÁ, L.; SÍČ, J.; VOJNAR, T. Fast Matching of Regular Patterns with Synchronizing Counting. In Foundations of Software Science and Computation Structures. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2023.
p. 392-412. ISSN: 0302-9743. Detail - KOZÁK, D.; JOVANOVIC, V.; STANCU, C.; VOJNAR, T.; WIMMER, C. Comparing Rapid Type Analysis with Points-To Analysis in GraalVM Native Image. In Proceedings of the 20th ACM SIGPLAN International Conference on Managed Programming Languages and Runtimes. New York: Association for Computing Machinery, 2023.
p. 129-142. ISBN: 979-8-4007-0380-5. Detail - MALÍK, V.; NEČAS, F.; SCHRAMMEL, P.; VOJNAR, T. 2LS: Arrays and Loop Unwinding (Competition Contribution). In Proceedings of the 29th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, part 2. Lecture Notes in Computer Science. Paris: Springer International Publishing, 2023.
p. 529-534. ISBN: 978-3-031-30819-2. Detail
Produkty
2024
- Predator Hunting Party: Nástroj pro verifikaci a hledání chyb, verze 3.1415, software, 2024
Autoři: MÜLLER, P.; PERINGER, P.; ŠOKOVÁ, V.; VOJNAR, T.; KINŠT, O.; KOTOUN, M.
2023
- 2LS: Nástroj pro statickou analýzu a verifikaci, verze 0.10, software, 2023
Autoři: KROENING, D.; MALÍK, V.; SCHRAMMEL, P.; VOJNAR, T.; MUKHERJEE, R.; MARTIČEK, Š.; NEČAS, F.; HRUŠKA, M.; BRAIN, M.; BUECHELI, S.; DAVID, C.; KUMAR, M.; WATCHER, B.