Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
Project goals
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.
Keywords
formal verificationsymbolic verificationinfinite-state systemstheory of automatalogicdynamic linked data structurescollectionsparametric systemsconcurrency
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 18 (SGA0201400001)
Main participants
Univerzita Karlova / Matematicko-fyzikální fakulta
Vysoké učení technické v Brně / Fakulta informačních technologiíContest type
VS - Public tender
Contract ID
14-11384S
Alternative language
Project name in Czech
Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí
Annotation in Czech
Projekt směřuje do oblasti formální verifikace nekonečně stavových softwarových systémů. Konkrétně se soustředí na zvýšení automatizace, škálovatelnosti a obecnosti současných metod formální verifikace programů s neomezenými datovými strukturami, jako jsou ukazatelové struktury a kolekce, obsahujícími data z případně neomezených domén a/nebo používající neomezený či parametrický paralelismus. V případě paralelních programů bude kladen důraz zejména na programy používající moderní synchronizační prostředky, jako jsou bezzámkové struktury či transakční paměti. S cílem umožnit verifikaci takových programů se projekt zaměřuje na rozvoj stávajících a návrh nových metod symbolické verifikace založených na využití automatů a logik. Při řešení projektu budou řešitelé konkrétně vycházet ze svých hlubokých a vzájemně se doplňujících zkušeností s abstraktním regulárním model checkingem, automaty nad stromy a lesy, separační logikou a symbolickými grafy paměti, predikátovou abstrakcí pro data a kolekce a vláknově modulární verifikací paralelních programů.
Scientific branches
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
The project contributed new results in the area of formal verification. The publication activity lagged significantly behind the original plan for journal papers, however, the results were published in relevant conferences, which is acceptable in the field of theoretical computer science. The high quality of the project results is also indicated by several prizes won at international competitions.
Solution timeline
Realization period - beginning
Jan 1, 2014
Realization period - end
Dec 31, 2016
Project status
U - Finished project
Latest support payment
May 4, 2016
Data delivery to CEP
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data delivery code
CEP17-GA0-GA-U/03:1
Data delivery date
Jun 28, 2017
Finance
Total approved costs
5,775 thou. CZK
Public financial support
5,775 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
5 775 CZK thou.
Public support
5 775 CZK thou.
100%
Provider
Czech Science Foundation
CEP
JC - Computer hardware and software
Solution period
01. 01. 2014 - 31. 12. 2016