Detail publikace
Byte-Precise Verification of Low-Level List Manipulation
symbolic memory graphs
Navrhujeme nový přístup k shape analýze programů s vázanými seznamy, které používají nízkoúrovňovou operace s pamětí. Takové operace zahrnují ukazatelovou aritmetiku, bezpečné používání neplatných ukazatelů, blokové operace s pamětí, reinterpretaci obsahu paměti, zarovnání adres, atd. Náš přístup je založený na nové reprezentaci množin hromad, který je do určité míry inspirován pracemi o separační logice se seznamovými predikáty vyššího řádu, ale je založený na grafech a používá mnohem jemnější (bytově přesný) paměťový model, aby podporoval výše zmíněné nízkoúrovňové operace s pamětí. Tento přístup byl implementován v nástroji Predator a úspěšně ověřen na mnoha netriviálních případových studiích, jejichž analýza je za hranicemi možností ostatních současných nástrojů na plně automatickou shape analýzu.
@techreport{BUT192900,
author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
title="Byte-Precise Verification of Low-Level List Manipulation",
year="2013",
publisher="Faculty of Information Technology BUT",
address="FIT-TR-2012-04, Brno",
pages="48",
url="http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/FIT-TR-2012-04.pdf"
}