Scalable Techniques for Analysis of Complex Properties of Computer Systems
Project goals
Due to the complexity of current software and the rising requirements on its reliability, traditional testing no longer suffices to assure the needed quality, and automated analysis and verification methods are needed. However, despite a lot of recent progress in this area, the current methods are still lacking in scalability, precision, and/or capabilities of analysing complex properties of advanced code. This is exactly what the project aims to attack, concentrating on several complementary types of program constructions that are particularly problematic for current automated analyses: namely, low-level pointer operations, dealing with arrays and strings, and concurrency. Both static approaches based on abstract interpretation and model checking as well as dynamic analysis based on extrapolation and noise injection will be studied. In the former case, a special attention will be devoted to approaches based on SAT/SMT solving, including improvements of the decision procedures used.
Keywords
automated analysis and verificationstatic analysisformal verificationdynamic analysisabstract interpretationmodel checkinginterpolating SAT/SMT solvinglow-level pointer programsprograms with arrays and stringsconcurrent programs
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
SGA0202000001
Main participants
Vysoké učení technické v Brně / Fakulta informačních technologií
Contest type
VS - Public tender
Contract ID
20-07487S
Alternative language
Project name in Czech
Škálovatelné techniky pro analýzu komplexních vlastností počítačových systémů
Annotation in Czech
S ohledem na složitost současného software a rostoucí požadavky na jeho spolehlivost jsou k dosažení jeho patřičné kvality vysoce zapotřebí automatizované metody analýzy a verifikace, klasické testování již nepostačuje. Ovšem přes značný pokrok v dané oblasti, současné metody analýzy a verifikace mají stále nedostatečnou škálovatelnost, přesnost, a/nebo nepokrývají složité vlastnosti pokročilých programových konstrukcí. Přesně na tyto nedostatky se zaměřuje předkládaný projekt, a to s důrazem na několik typů programových konstrukcí problematických pro současné analýzy: konkrétně nízko-úrovňovou práci s ukazateli, práci s poli a řetězci a paralelismus. Budou přitom uvažovány jak statické přístupy založené na abstraktní interpretaci a model checkingu, tak i dynamická analýza s využitím extrapolace a vkládání šumu. V případě statických přístupů bude zvláštní důraz kladen na přístupy využívající řešení SAT/SMT problémů, včetně zdokonalení příslušných rozhodovacích procedur.
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
—
OECD FORD - another secondary branch
—
AF - Documentation, librarianship, work with information
BC - Theory and management systems
BD - Information theory
IN - Informatics
Solution timeline
Realization period - beginning
Jan 1, 2020
Realization period - end
Dec 31, 2022
Project status
—
Latest support payment
Apr 12, 2022
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
CEP23-GA0-GA-R
Data delivery date
Jun 26, 2023
Finance
Total approved costs
10,611 thou. CZK
Public financial support
9,278 thou. CZK
Other public sources
1,278 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
10 611 CZK thou.
Public support
9 278 CZK thou.
87%
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. 2020 - 31. 12. 2022