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

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

Information

This project doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official project website can be found on muni.cz.
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.