Correctness Analysis of C and C++ Programs with Threads
Project goals
The goal of this project is to research and develop new algorithms and data structures to support model checking of multi-threaded programs written in the C and C++ programming languages. The particular goals of the project include the development of new techniques for automated program abstraction by means of program transformation, techniques for efficient combination of explicit and symbolic approaches to model checking. We will also seek additional techniques for reducing memory requirements of formal verification tools, model checkers in particular. The newly developed data structures and algorithms will be implemented and evaluated within the context of the parallel LTL model checker DIVINE. Our intent is to push the tractability frontier in the area of multi-threaded C and C++ programs, taking advantage of contemporary computational platforms such as multi-core workstations or high-performance clusters.
Keywords
formal verificationliner temporal logicparallel and distributed model checkingLLVM bitcode
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 19 (SGA0201500001)
Main participants
Masarykova univerzita / Fakulta informatiky
Contest type
VS - Public tender
Contract ID
15-08772S
Alternative language
Project name in Czech
Analýza korektnosti vícevláknových programů v C a C++
Annotation in Czech
Projekt se zaměřuje na výzkum a vývoj nových algoritmů a datových struktur, které umožní efektivní verifikaci vícevláknových programů zapsaných v programovacích jazycích C a C++ metodou ověřování modelu (angl. model checking). Konkrétním cílem projektu je vyvinout nové metody automatické abstrakce programů vstupujících do procesu verifikace, které budou realizované formou transformace těchto programů. Dále pak získat nové metody umožňující kombinaci explicitního a symbolického přístupu k verifikaci metodou ověřování modelu, či metody umožňující jiným způsobem redukovat prostorové nároky verifikačních nástrojů. Pro účely porovnání a vyhodnocení budou nově vyvinuté algoritmy a datové struktury integrovány do experimentálního softwarového nástroje DIVINE. To mimo jiné umožní efektivní využití stávajících výpočetních architektur (více-jádrové počítače, výpočetní klastry) tak, aby byla významně posunuta hranice systémů, jež je možné verifikovat automatizovanými metodami formální verifikace.
Scientific branches
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 brings new results in the area of automatic formal verification by model checking published in 12 conference and 3 journal (Jimp) papers of an acceptable quality. The proposed methods were implemented within the tool DIVINE and analyzed experimentally. Students of distinct study programs were involved in the project actively. Finances were exploited effectively.
Solution timeline
Realization period - beginning
Jan 1, 2015
Realization period - end
Dec 31, 2017
Project status
U - Finished project
Latest support payment
Apr 5, 2017
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
CEP18-GA0-GA-U/02:1
Data delivery date
May 4, 2018
Finance
Total approved costs
4,998 thou. CZK
Public financial support
4,998 thou. CZK
Other public sources
0 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
4 998 CZK thou.
Public support
4 998 CZK thou.
100%
Provider
Czech Science Foundation
CEP
IN - Informatics
Solution period
01. 01. 2015 - 31. 12. 2017