Detail publikace

Byte-Precise Verification of Low-Level List Manipulation

DUDKA Kamil, PERINGER Petr a VOJNAR Tomáš. Byte-Precise Verification of Low-Level List Manipulation. In: 20th Static Analysis Symposium. Lecture Notes in Computer Science Volume 7935, roč. 20. Berlin: Springer Verlag, 2013, s. 215-237. ISBN 978-3-642-38855-2. ISSN 0302-9743.
Název česky
Nízkoúrovňová verifikace manipulace seznamů
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Dudka Kamil, Ing. (UITS FIT VUT)
Peringer Petr, Dr. Ing. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
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
215-237
Časopis
Lecture Notes in Computer Science, roč. 20, č. 7935, ISSN 0302-9743
Sborník
20th Static Analysis Symposium
Řada
Lecture Notes in Computer Science Volume 7935
Konference
20th International Static Analysis Symposium -- SAS 2013, Seattle, Washington, US
ISBN
978-3-642-38855-2
Vydavatel
Springer Verlag
Místo
Berlin, DE
BibTeX 
@INPROCEEDINGS{FITPUB10329,
   author = "Kamil Dudka and Petr Peringer and Tom\'{a}\v{s} Vojnar",
   title = "Byte-Precise Verification of Low-Level List Manipulation",
   pages = "215--237",
   booktitle = "20th Static Analysis Symposium",
   series = "Lecture Notes in Computer Science Volume 7935",
   journal = "Lecture Notes in Computer Science",
   volume = 20,
   number = 7935,
   year = 2013,
   location = "Berlin, DE",
   publisher = "Springer Verlag",
   ISBN = "978-3-642-38855-2",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/10329"
}
Nahoru