Detail publikace

Template-Based Verification of Heap-Manipulating Programs

HRUŠKA, M.; MALÍK, V.; SCHRAMMEL, P.; VOJNAR, T. Template-Based Verification of Heap-Manipulating Programs. In Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2018. p. 103-111. ISBN: 978-0-9835678-8-2.
Název česky
Verifikace založená na šablonách pro programy pracující s haldou
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Hruška Martin, Ing., Ph.D. (VZ Automata@FIT)
Malík Viktor, Ing., Ph.D. (UITS)
Schrammel Peter
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

software analysis, software verification, shape analysis, template based verification, 2LS, love, domain combination

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
DOI
10.23919/FMCAD.2018.8603009
UT WoS
000493916300018
EID Scopus
2-s2.0-85061627483
BibTeX 
@inproceedings{BUT155109,
  author="Martin {Hruška} and Viktor {Malík} and Peter {Schrammel} and Tomáš {Vojnar}",
  title="Template-Based Verification of Heap-Manipulating Programs",
  booktitle="Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design",
  year="2018",
  pages="103--111",
  publisher="FMCAD Inc.",
  address="Austin",
  doi="10.23919/FMCAD.2018.8603009",
  isbn="978-0-9835678-8-2",
  url="https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf"
}
Nahoru