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.