Abstraction and Other Techniques in Semi-Symbolic Program Verification

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

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.

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

—

CEP - equivalent branches <br>(according to the <a href="http://www.vyzkum.cz/storage/att/E6EF7938F0E854BAE520AC119FB22E8D/Prevodnik_oboru_Frascati.pdf">converter</a>)

AF - Documentation, librarianship, work with information<br>BC - Theory and management systems<br>BD - Information theory<br>IN - Informatics

Realization period - beginning

Jan 1, 2018

Realization period - end

Dec 31, 2020

Project status

—

Latest support payment

Apr 24, 2020

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

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