Detail publikace

Template-Based Verification of Heap-Manipulating Programs

HRUŠKA Martin, MALÍK Viktor, SCHRAMMEL Peter a VOJNAR Tomáš. Template-Based Verification of Heap-Manipulating Programs. In: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2018, s. 103-111. ISBN 978-0-9835678-8-2. Dostupné z: https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf
Název česky
Verifikace založená na šablonách pro programy pracující s haldou
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Hruška Martin, Ing. (UITS FIT VUT)
Malík Viktor, Ing. (UITS FIT VUT)
Schrammel Peter, Dr. (US)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
URL
Abstrakt

Práce předkláda analýzu tvarů haldy vhodnou pro verifikační metodu založenou na SMT solvrech. Řešení spočívá v abstraktních šablonách haldy, které kódují tvary haldy do logických formulí nad bit-vectory. Naši abstraktní doménu lze snadno kombinovat s doménami pro číselné hodnoty tak, aby bylo možné verifikovat vlastnosti hodnot uložených v datových strukturách. Naše metoda byla porovnána s ostatními nástroji pro analýzu tvaru, které se účastnily známé soutěže SV-COMP. Porovnání proběhlo na příkladech, které vyžadovaly usuzování jak o tvarech haldy, tak hodnotách na haldě uložených. Náš nástroj 2LS překonal nástroje konkurenční ve verifikaci zmíněných příkladů.

Rok
2018
Strany
103-111
Sborník
Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design
Konference
Formal Methods in Computer-Aided Design, Austin, Texas, US
ISBN
978-0-9835678-8-2
Vydavatel
FMCAD Inc.
Místo
Austin, US
DOI
UT WoS
000493916300018
EID Scopus
BibTeX
@INPROCEEDINGS{FITPUB11861,
   author = "Martin Hru\v{s}ka and Viktor Mal\'{i}k and Peter Schrammel and Tom\'{a}\v{s} Vojnar",
   title = "Template-Based Verification of Heap-Manipulating Programs",
   pages = "103--111",
   booktitle = "Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design",
   year = 2018,
   location = "Austin, US",
   publisher = "FMCAD Inc.",
   ISBN = "978-0-9835678-8-2",
   doi = "10.23919/FMCAD.2018.8603009",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11861"
}
Nahoru