Přejít k obsahu | Přejít k hlavnímu menu | Přejít k vyhledávání

Informace o projektu
Abstrakce a jiné techniky v semi-symbolické verifikaci programů

Logo poskytovatele
Kód projektu
GA18-02177S
Období řešení
1/2018 - 12/2020
Investor / Programový rámec / typ projektu
Grantová agentura ČR
  • Standardní projekty
Fakulta / Pracoviště MU
Fakulta informatiky

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.

Publikace

Počet publikací: 22

2021

2020

2019

Předchozí 1 2 3 Další

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.

Další info