Detail projektu

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

Období řešení: 1. 1. 2014 - 31. 12. 2016

Typ projektu: grant

Kód: GA14-11384S

Agentura: Grantová agentura České republiky

Program: Standardní projekty

Název anglicky
Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
Typ
grant
Klíčová slova

formální verifikace, symbolická verifikace, nekonečně stavové systémy, teorie automatů, logika, dynamické struktury založené na ukazatelích, kolekce, parametrické systémy, paralelismus

Abstrakt

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 jeho řešení 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ů.

Řešitelé
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT) , hlavní řešitel
Kofroň Jan, doc. RNDr., Ph.D. (MFF UK) , spoluřešitel
Dudka Kamil, Ing. (UITS FIT VUT)
Fiedor Jan, Ing., Ph.D. (UITS FIT VUT)
Holík Lukáš, doc. Mgr., Ph.D. (UITS FIT VUT)
Hruška Martin, Ing., Ph.D. (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)
Publikace

2017

2016

2015

2014

Produkty

2015

2014

Nahoru