Detail publikace

Byte-Precise Verification of Low-Level List Manipulation

DUDKA, K.; PERINGER, P.; VOJNAR, T. Byte-Precise Verification of Low-Level List Manipulation. FIT-TR-2012-04, Brno: Faculty of Information Technology BUT, 2013. p. 0-0.
Název česky
Nízkoúrovňová verifikace manipulace seznamů
Typ
zpráva odborná
Jazyk
anglicky
Autoři
Dudka Kamil, Ing.
Peringer Petr, Dr. Ing. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

dynamic linked data structuresseparation logic
symbolic memory graphslist manipulationlow-level memory manipulationmemory
safetyshape analysis

Abstrakt

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.

Rok
2013
Strany
48
Vydavatel
Faculty of Information Technology BUT
Místo
FIT-TR-2012-04, Brno
BibTeX 
@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"
}
Nahoru