Project Details

Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí

Project Period: 1. 1. 2014 - 31. 12. 2016

Project Type: grant

Code: GA14-11384S

Agency: Czech Science Foundation

Program: Standardní projekty

English title
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures

formal verification, symbolic verification, infinite-state systems, theory of automata, logic, dynamic linked data structures, collections, parametric systems, concurrency


The project targets formal verification of infinite-state software systems. In particular, it aims at improving the degree of automation, scalability, and generality of the current approaches to formal verification of programs handling unbounded data structures, such as collections or dynamic linked data structures based on pointers, possibly storing data from unbounded domains, and/or using unbounded or parametric concurrency. As for concurrent programs, the stress will be on programs using modern synchronization means such as lockless data structures or transactional memories. To handle such programs, the project focuses on extending the current and developing new symbolic verification approaches based on automata and/or logics. When working on the project, members of the project teams will build on their deep and mutually complementary expertise with abstract regular model checking, tree and forest automata, separation logic and symbolic memory graphs, predicate abstraction over primitive data and collections, and thread modular verification of concurrent programs.

Team members
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , research leader
Kofroň Jan, RNDr., Ph.D. (MFF UK) , team leader
Dudka Kamil, Ing. (UITS FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, Mgr., Ph.D. (UITS FIT VUT)
Hruška Martin, Ing. (FIT VUT)
Chaloupka Jan, Ing. (UITS FIT VUT)
Charvát Lukáš, Ing. (UITS FIT VUT)
Lengál Ondřej, Ing., Ph.D. (UITS FIT VUT)
Müller Petr, Ing. (UITS FIT VUT)
Parízek Pavel, RNDr., Ph.D. (MFF UK)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Rogalewicz Adam, doc. Mgr., Ph.D. (UITS FIT VUT)








Back to top