Verification and Bug Hunting for Advanced Software
Project goals
Automated software verification and bug hunting are hot topics in both industry and academia. Indeed, they can save a lot of money and, in case of safety-critical software, even human lives. This project aims at new automated methods of static formal verification (based on approaches such as symbolic verification and automated abstraction) as well as extrapolating dynamic analysis and advanced testing of programs that use several classes of advanced programming constructions. In particular, the project concentrates on pointer programs, concurrent programs (including cloud programs), and container programs. While these areas are to some degree independent, there is also a lot of overlap among them: On the one hand, one needs to consider various combinations of the mentioned constructions (e.g., concurrent pointer programs). On the other hand, one needs to solve similar problems for all of them. An important example of the latter considered in the project is dealing with open programs, i.e., program fragments that the programmers need to verify despite their environment is unknown.
Keywords
formal verificationstatic analysissymbolic verificationautomated abstractiondynamic analysis and testingnoise injectionmodel-based testingautomatalogicspointer programsconcurrent programscontainer programs
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 21 (SGA0201700001)
Main participants
Univerzita Karlova / Matematicko-fyzikální fakulta
Vysoké učení technické v Brně / Fakulta informačních technologiíContest type
VS - Public tender
Contract ID
17-12465S
Alternative language
Project name in Czech
Verifikace a hledání chyb v pokročilém softwaru
Annotation in Czech
Automatizovaná verifikace a vyhledávání chyb v softwaru patří mezi témata aktivně řešená jak na univerzitách tak v průmyslu. Konečně tyto techniky mohou ušetřit značné finanční prostředky a u bezpečnostně kritických aplikací také lidské životy. Cílem tohoto projektu jsou nové automatizované metody statické formální verifikace (založené na metodách jako symbolická verifikace či automatická abstrakce) i extrapolující dynamické analýzy a pokročilého testování, a to pro programy používající několik různých pokročilých programovacích technik. Konkrétně se projekt zaměřuje na programy s ukazateli, paralelní programy (včetně cloudových) a programy s kontejnery. Tyto oblasti jsou sice částečně nezávislé, ale také se do značné míry překrývají: Na jednu stranu je zapotřebí zvládnout různé kombinace uvedených konstrukcí (např. paralelní programy s ukazateli) a na druhou stranu je zapotřebí ve všech těchto oblastech řešit podobné problémy. Důležitým příkladem takového problému, který bude řešen v projektu, je potřeba verifikovat otevřené programy, tedy fragmenty kódu, jejichž okolí není známo.
Scientific branches
Completed project evaluation
Provider evaluation
V - Vynikající výsledky projektu (s mezinárodním významem atd.)
Project results evaluation
The project has focused on methods of static and dynamic analysis of programs with pointers, concurrency and containers. The research tasks outlined for the project were well developed, a number of research results were produced and published in good conferences and journals, and some of them led to best-paper awards.
Solution timeline
Realization period - beginning
Jan 1, 2017
Realization period - end
Dec 31, 2019
Project status
U - Finished project
Latest support payment
Apr 26, 2019
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
CEP20-GA0-GA-U/02:1
Data delivery date
Jul 23, 2020
Finance
Total approved costs
8,912 thou. CZK
Public financial support
7,448 thou. CZK
Other public sources
1,396 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
8 912 CZK thou.
Public support
7 448 CZK thou.
83%
Provider
Czech Science Foundation
CEP
JC - Computer hardware and software
Solution period
01. 01. 2017 - 31. 12. 2019