Go to main content | Go to main menu | Go to search

Project information
Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Investor logo
Project Identification
GA18-02177S
Project Period
1/2018 - 12/2020
Investor / Pogramme / Project type
Czech Science Foundation
  • Standard Projects
MU Faculty or unit
Faculty of Informatics

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.

Publications

Total number of publications: 22

2021

2020

2019

Previous 1 2 3 Next

You are running an old browser version. We recommend updating your browser to its latest version.

More info