Abstraction and Other Techniques in Semi-Symbolic Program Verification
Project goals
This project aims at research and development of new algorithms and data structures to enable efficient analysis and verification of computer programs written in the C/C++ programming languages. One of the particular goals of the project is to employ abstractions that are realised as speculative assume statements in the source-code of the program. Programs annotated with such speculative asssumptions are easier to verify. However, invalid speculation may lead to an incorrect verification result. The goal of the project is to build a theory of speculative assumptions, the validity of which can be easily determined during the verification process itself, and to materialise this theory in a verification tool/framework. This framework will additionaly employ other program analysis and verification techniques (slicing, SMT solving, etc.) to make the entire process of program analysis and program verification more efficient.
Keywords
source-code verificationmodel checkingsymbolic executionabstractionSMT-solving
Public support
Provider
Czech Science Foundation
Programme
Standard projects
Call for proposals
Standardní projekty 22 (SGA0201800001)
Main participants
Masarykova univerzita / Fakulta informatiky
Contest type
VS - Public tender
Contract ID
18-02177S
Alternative language
Project name in Czech
Abstrakce a jiné techniky v semi-symbolické verifikaci programů
Annotation in Czech
Projekt se zaměřuje na výzkum a vývoj nových algoritmů a datových struktur, které umožní efektivní analýzu a verifikaci počítačových programů zapsaných v programovacích jazycích C a C++. Konkrétně se projekt zaměřuje na využití abstrakcí, které jsou realizované jako spekulativní předpoklady kladené na běh verifikovaného programu. Programy, které jsou anotovány spekulativními předpoklady, je méně náročné verifikovat, avšak v případě předpokladů, které nejsou pravdivé, může být výsledek verifikace nekorektní. Cílem projektu je vystavět teorii spekulativních předpokladů, jejichž neplatnost bude možné detekovat samotnou procedurou verifikace, a tuto teorii realizovat ve vhodném verifikačním prostředí. Toto prostředí bude nad rámec uvedené metody zahrnovat využití dalších relevantních technik verifikace a analýzy programů (prořezávání kódu, řešení SMT dotazů, a pod.), které v souhrnu povedou k větší efektivitě procedury verifikace.
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, 2018
Realization period - end
Dec 31, 2020
Project status
—
Latest support payment
Apr 24, 2020
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
CEP21-GA0-GA-R/11:1
Data delivery date
Feb 22, 2021
Finance
Total approved costs
6,232 thou. CZK
Public financial support
4,562 thou. CZK
Other public sources
1,740 thou. CZK
Non public and foreign sources
0 thou. CZK
Basic information
Recognised costs
6 232 CZK thou.
Public support
4 562 CZK thou.
73%
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. 2018 - 31. 12. 2020