Project information
Advanced Analysis and Verification for Advanced Software
(AIDE)
- Project Identification
- GA23-06506S
- Project Period
- 1/2023 - 12/2025
- Investor / Pogramme / Project type
-
Czech Science Foundation
- Standard Projects
- MU Faculty or unit
- Faculty of Informatics
- Cooperating Organization
-
Charles University
- Responsible person doc. RNDr. Jan Kofroň, Ph.D.
- Responsible person prof. Ing. Tomáš Vojnar, Ph.D.
To help software developers to cope with the huge and ever-increasing complexity of software, the project aims at new techniques of automated analysis and verification of advanced software, which uses low-level programming, new high-level constructs, or both. To obtain such methods, the project intends to build primarily on various logic-based approaches, such as biabductive analysis or symbolic execution, suitably combined with methods like abstract interpretation, slicing, and advanced type systems. To increase the efficiency of the considered logic-based methods, the project will also develop or significantly improve decision procedures for the various considered logics (e.g., separation logic, quantified bit-vector logic, or constrained Horn clauses). The low-level programs to be verified include especially programs with low-level pointer manipulation and dynamic-linked data structures, while the considered high-level programs include programs based on expert systems, high-level specifications of software, and programs in modern high-level languages like Scala.
Sustainable Development Goals
Masaryk University is committed to the UN Sustainable Development Goals, which aim to improve the conditions and quality of life on our planet by 2030.
Publications
Total number of publications: 13
2025
-
Compositional Shape Analysis with Shared Abduction and Biabductive Loop Acceleration
Proc. of the 34th European Symposium on Programming – ESOP'25, year: 2025
-
Data Race Detection with Frama-C (Competition Contribution)
Proc. of 31st International Conference on Tools and Algorithms for the Construction and Analysis of Systems – TACAS'25 as a competition contribution within the 14th International Competition on Software Verification – SV-COMP'25, year: 2025
-
RacerF: Lightweight Static Data Race Detection for C Code (Experience Paper)
Proc. of 39th European Conference on Object-Oriented Programming – ECOOP'25, year: 2025
-
SkipFlow: Improving the Precision of Points-to Analysis Using Primitive Values and Predicate Edges
Proc. of the 23rd ACM/IEEE International Symposium on Code Generation and Optimization – CGO'25, year: 2025
-
Software Verification Witnesses 2.0
Model Checking Software - 30th International Symposium, SPIN 2024, year: 2025
2024
-
Combining Symbolic Execution with Predicate Abstraction and CEGAR
Proceedings of the 24th Conference on Formal Methods in Computer-Aided Design – FMCAD 2024, year: 2024
-
Fizzer: New Gray-Box Fuzzer
Fundamental Approaches to Software Engineering - 27th International Conference, FASE 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, year: 2024
-
Gray-Box Fuzzing via Gradient Descent and Boolean Expression Coverage
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, year: 2024
-
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, year: 2024
-
Tighter Construction of Tight Büchi Automata
Foundations of Software Science and Computation Structures - 27th International Conference, FoSSaCS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part I, year: 2024