Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 13 (SGA02010GA-ST)
Main participants
—
Contest type
VS - Public tender
Contract ID
P103-10-0306
Alternative language
Project name in Czech
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti
Annotation in Czech
Automatizovaná verifikace programů je v současnosti s ohledem na rostoucí dopad počítačem řízených systémů na naše životy a výraznou potřebu minimalizovat počet chyb v těchto systémech velmi aktuálním výzkumným tématem. Projekt se konkrétně zaměřuje na verifikaci programů s pokročilými rysy paralelismu a neomezenosti, které patří k obzvláště problematickým aspektům software, se kterými se musí automatická verifikace vyrovnávat. V prvním případě se projekt soustřeďuje zejména na metody verifikace programů určených pro moderní vícejádrové procesory. V druhém případě se jedná o verifikaci programů pracujících s různými neomezenými datovými strukturami, zejména pak poli (o parametrické velikosti) a složitými dynamickými strukturami založenými na ukazatelích (jako jsou seznamy či stromy). Projekt zahrnuje výzkum metod dynamické i statické verifikace, včetně model checkingu, a také jejích vhodných kombinací. Pro práci s programy s nekonečnými stavovými prostory se výzkum v projektu zaměřuje na metody efektivní symbolické verifikace založené na použití automatů a logik.
Scientific branches
R&D category
ZV - Basic research
CEP classification - main branch
JC - Computer hardware and software
CEP - secondary branch
IN - Informatics
CEP - another secondary branch
—
OECD FORD - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)<br>20206 - Computer hardware and architecture
Completed project evaluation
Provider evaluation
U - Uspěl podle zadání (s publikovanými či patentovanými výsledky atd.)
Project results evaluation
The project has brought internationally recognized results in the formal verification of programs with various sources of unboundedness and of concurrent programs. These were high quality publications in journals (7) and at international conferences (31), as well as publicly available software tools for experiments in program verification. Three conference papers received a best paper award.
Solution timeline
Realization period - beginning
Jan 1, 2010
Realization period - end
Dec 31, 2013
Project status
U - Finished project
Latest support payment
Jun 12, 2013
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
CEP14-GA0-GA-U/01:1
Data delivery date
Jul 1, 2014
Finance
Total approved costs
4,752 thou. CZK
Public financial support
4,752 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK