Project information
Advanced Analysis and Verification for Advanced Software (AIDE)

Investor logo
Project Identification
Project Period
1/2023 - 12/2025
Investor / Pogramme / Project type
Czech Science Foundation
MU Faculty or unit
Faculty of Informatics
Cooperating Organization
Charles University
Brno University of Technology

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.

Sustainable Development Goal No.  9 – Industry, innovation and infrastructure Sustainable Development Goal No.  16 – Peace, justice and strong institutions


Total number of publications: 6

You are running an old browser version. We recommend updating your browser to its latest version.

More info