Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Cíle projektu
Projekt se zaměřuje na výzkum a vývoj nových algoritmů a datových struktur, které umožní efektivní analýzu a verifikaci počítačových programů zapsaných v programovacích jazycích C a C++. Konkrétně se projekt zaměřuje na využití abstrakcí, které jsou realizované jako spekulativní předpoklady kladené na běh verifikovaného programu. Programy, které jsou anotovány spekulativními předpoklady, je méně náročné verifikovat, avšak v případě předpokladů, které nejsou pravdivé, může být výsledek verifikace nekorektní. Cílem projektu je vystavět teorii spekulativních předpokladů, jejichž neplatnost bude možné detekovat samotnou procedurou verifikace, a tuto teorii realizovat ve vhodném verifikačním prostředí. Toto prostředí bude nad rámec uvedené metody zahrnovat využití dalších relevantních technik verifikace a analýzy programů (prořezávání kódu, řešení SMT dotazů, a pod.), které v souhrnu povedou k větší efektivitě procedury verifikace.
Klíčová slova
source-code verificationmodel checkingsymbolic executionabstractionSMT-solving
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
Standardní projekty 22 (SGA0201800001)
Hlavní účastníci
Masarykova univerzita / Fakulta informatiky
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
18-02177S
Alternativní jazyk
Název projektu anglicky
Abstraction and Other Techniques in Semi-Symbolic Program Verification
Anotace anglicky
This project aims at research and development of new algorithms and data structures to enable efficient analysis and verification of computer programs written in the C/C++ programming languages. One of the particular goals of the project is to employ abstractions that are realised as speculative assume statements in the source-code of the program. Programs annotated with such speculative asssumptions are easier to verify. However, invalid speculation may lead to an incorrect verification result. The goal of the project is to build a theory of speculative assumptions, the validity of which can be easily determined during the verification process itself, and to materialise this theory in a verification tool/framework. This framework will additionaly employ other program analysis and verification techniques (slicing, SMT solving, etc.) to make the entire process of program analysis and program verification more efficient.
Vědní obory
Kategorie VaV
ZV - Základní výzkum
OECD FORD - hlavní obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - vedlejší obor
—
OECD FORD - další vedlejší obor
—
CEP - odpovídající obory
(dle převodníku)AF - Dokumentace, knihovnictví, práce s informacemi
BC - Teorie a systémy řízení
BD - Teorie informace
IN - Informatika
Termíny řešení
Zahájení řešení
1. 1. 2018
Ukončení řešení
31. 12. 2020
Poslední stav řešení
—
Poslední uvolnění podpory
24. 4. 2020
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
CEP21-GA0-GA-R/11:1
Datum dodání záznamu
22. 2. 2021
Finance
Celkové uznané náklady
6 232 tis. Kč
Výše podpory ze státního rozpočtu
4 562 tis. Kč
Ostatní veřejné zdroje financování
1 740 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
6 232 tis. Kč
Statní podpora
4 562 tis. Kč
73%
Poskytovatel
Grantová agentura České republiky
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Doba řešení
01. 01. 2018 - 31. 12. 2020