Automatizovaná formální analýza a verifikace programů se složitými datovými a řídicími strukturami s předem neomezenou velikostí
Cíle projektu
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ů.
Klíčová slova
formal verificationsymbolic verificationinfinite-state systemstheory of automatalogicdynamic linked data structurescollectionsparametric systemsconcurrency
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
Standardní projekty 18 (SGA0201400001)
Hlavní účastníci
Univerzita Karlova / Matematicko-fyzikální fakulta
Vysoké učení technické v Brně / Fakulta informačních technologiíDruh soutěže
VS - Veřejná soutěž
Číslo smlouvy
14-11384S
Alternativní jazyk
Název projektu anglicky
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
Anotace anglicky
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.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
CEP - hlavní obor
JC - Počítačový hardware a software
CEP - vedlejší obor
—
CEP - další vedlejší obor
—
OECD FORD - odpovídající obory
(dle převodníku)20206 - Computer hardware and architecture
Hodnocení dokončeného projektu
Hodnocení poskytovatelem
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Zhodnocení výsledků projektu
Projekt přinesl nové výsledky v obasti formální verifikace. Publikační aktivita významně zaostala za původním plánem časopisových publikací, ale výsledky byly zveřejněny na relevantních konferencích, což je v případě teoretické informatiky přijatelné. O kvalitě výsledků projektu svědčí i několik ocenění vyvinutých metod v mezinárodních soutěžích.
Termíny řešení
Zahájení řešení
1. 1. 2014
Ukončení řešení
31. 12. 2016
Poslední stav řešení
U - Ukončený projekt
Poslední uvolnění podpory
4. 5. 2016
Dodání dat do CEP
Důvěrnost údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Systémové označení dodávky dat
CEP17-GA0-GA-U/03:1
Datum dodání záznamu
28. 6. 2017
Finance
Celkové uznané náklady
5 775 tis. Kč
Výše podpory ze státního rozpočtu
5 775 tis. Kč
Ostatní veřejné zdroje financování
0 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
5 775 tis. Kč
Statní podpora
5 775 tis. Kč
100%
Poskytovatel
Grantová agentura České republiky
CEP
JC - Počítačový hardware a software
Doba řešení
01. 01. 2014 - 31. 12. 2016