Advanced Analysis and Verification for Advanced Software
Project goals
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.
Keywords
automated analysis and verificationlogicabductionsymbolic executionabstract interpretationslicingSMTdecision proceduresseparation logicbitvector logicconstrained Horn clauseslow-level programminghigh-level languages and specifications
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
SGA0202300001
Main participants
Vysoké učení technické v Brně / Fakulta informačních technologií
Contest type
VS - Public tender
Contract ID
23-06506S
Alternative language
Project name in Czech
Pokročilá analýza a verifikace pro pokročilý software
Annotation in Czech
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.
Scientific branches
R&D category
ZV - Basic research
OECD FORD - main branch
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
OECD FORD - secondary branch
20206 - Computer hardware and architecture
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
JC - Computer hardware and software
Solution timeline
Realization period - beginning
Jan 1, 2023
Realization period - end
Dec 31, 2025
Project status
K - Ending multi-year project
Latest support payment
Feb 29, 2024
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
CEP25-GA0-GA-R
Data delivery date
Feb 21, 2025
Finance
Total approved costs
13,285 thou. CZK
Public financial support
10,970 thou. CZK
Other public sources
2,211 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
13 285 CZK thou.
Public support
10 970 CZK thou.
82%
Provider
Czech Science Foundation
OECD FORD
Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Solution period
01. 01. 2023 - 31. 12. 2025