Detail publikace
Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
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{BUT21471,
author="Pavel {Erlebach} and Tomáš {Vojnar}",
title="Automated Formal Verification of Programs with Dynamic Data Structures Using State-of-the-Art Tools",
booktitle="Proceedings of 8th International Conference ISIM'05 Information System Implementation and Modeling",
year="2005",
pages="219--226",
address="Ostrava",
isbn="80-86840-09-3"
}