Detail publikace
Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools
automatická formální verifikace, TVLA, PALE, úplná uspořádanost, insertBST
Tento článek zkoumá možnosti dvou pokročilých automatických prostředků (jmenovitě TVLA a PALE) pro verifikaci systémů pracujících s neomezenými dynamickými datovými strukturami. Uvažujeme verifikaci procedur pracujících s binárními seřazenými stromy, kde chceme zverifikovat základní požadavky správnosti ukazatelových operací (dereference přes null atd.) a dále i požadavek úplné uspořádanosti zmíněných stromů, tj. všechny uzly levého podstromu uzlu n jsou menší než n a všechny uzly pravého podstromu uzlu n jsou větší než n (čili nezkoumáme jen vztah uzlu a jeho následníků). Abychom byli schopni zverifikovat tuto vlastnost v TVLA, představíme nový instrumentační predikát, který je schopen tuto vlastnost u příslušné procedury zverifikovat.
@INPROCEEDINGS{FITPUB7752,
author = "Pavel Erlebach and Tom\'{a}\v{s} Vojnar",
title = "Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools",
pages = "219--226",
booktitle = "Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling",
year = 2005,
location = "Ostrava, CZ",
ISBN = "80-86840-09-3",
language = "english",
url = "https://www.fit.vut.cz/research/publication/7752"
}