Pokročilá analýza a verifikace pro pokročilý software
Cíle projektu
S cílem pomoci vývojářům software vyrovnat se s jeho obrovskou a stále rostoucí složitostí se projekt zaměřuje na nové metody automatizované analýzy a verifikace pokročilého software, založeného na nízkoúrovňovém programování, moderních vysokoúrovňových přístupech či obojím. Projekt bude rozvíjet zejména metody založené na logice, jako je bi-abduktivní analýza nebo symbolické provádění, vhodně kombinované s přístupy, jako je abstraktní interpretace, „slicing“ či pokročilé typové systémy. Pro zefektivnění uvažovaných metod založených na logice budou rovněž vyvíjeny rozhodovací procedury pro různé uvažované logiky (např. separační logiku, kvantifikovanou bit-vektorovou logiku či Hornovy klauzule s omezeními). Mezi nízkoúrovňové programy, jež jsou cílem vyvíjených verifikačních metod, patří zejména programy využívající nízkoúrovňovou manipulaci s ukazateli a dynamickými datovými strukturami, zatímco mezi uvažované vysokoúrovňové programy patří programy založené na expertních systémech, vysokoúrovňové specifikace software či programy v moderních vysokoúrovňových jazycích, jako je Scala.
Klíčová slova
automated analysis and verificationlogicabductionsymbolic executionabstract interpretationslicingSMTdecision proceduresseparation logicbitvector logicconstrained Horn clauseslow-level programminghigh-level languages and specifications
Veřejná podpora
Poskytovatel
Grantová agentura České republiky
Program
Standardní projekty
Veřejná soutěž
SGA0202300001
Hlavní účastníci
Vysoké učení technické v Brně / Fakulta informačních technologií
Druh soutěže
VS - Veřejná soutěž
Číslo smlouvy
23-06506S
Alternativní jazyk
Název projektu anglicky
Advanced Analysis and Verification for Advanced Software
Anotace anglicky
To help software developers to cope with the huge and ever-increasing complexity of software, the project aims at new techniques of automated analysis and verification of advanced software, which uses low-level programming, new high-level constructs, or both. To obtain such methods, the project intends to build primarily on various logic-based approaches, such as bi-abductive analysis or symbolic execution, suitably combined with methods like abstract interpretation, slicing, and advanced type systems. To increase the efficiency of the considered logic-based methods, the project will also develop or significantly improve decision procedures for the various considered logics (e.g., separation logic, quantified bit-vector logic, or constrained Horn clauses). The low-level programs to be verified include especially programs with low-level pointer manipulation and dynamic-linked data structures, while the considered high-level programs include programs based on expert systems, high-level specifications of software, and programs in modern high-level languages like Scala.
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
20206 - Computer hardware and architecture
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
JC - Počítačový hardware a software
Termíny řešení
Zahájení řešení
1. 1. 2023
Ukončení řešení
31. 12. 2025
Poslední stav řešení
K - Končící víceletý projekt
Poslední uvolnění podpory
29. 2. 2024
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
CEP25-GA0-GA-R
Datum dodání záznamu
21. 2. 2025
Finance
Celkové uznané náklady
13 285 tis. Kč
Výše podpory ze státního rozpočtu
10 970 tis. Kč
Ostatní veřejné zdroje financování
2 211 tis. Kč
Neveřejné tuz. a zahr. zdroje finan.
0 tis. Kč
Základní informace
Uznané náklady
13 285 tis. Kč
Statní podpora
10 970 tis. Kč
82%
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. 2023 - 31. 12. 2025