Detail publikace
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)
DUDKA, K. MÜLLER, P. PERINGER, P. VOJNAR, T.
Originální název
Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)
Typ
článek v časopise - ostatní, Jost
Jazyk
angličtina
Originální abstrakt
Predator is a tool for automated formal verification of sequential C programs with dynamic linked data structures. It is in principle based on separation logic, but uses a graph-based heap representation. This paper first provides a brief overview of Predator and then discusses experience with its participation in the Software Verification Competition of TACAS'12.
Klíčová slova
separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists, Competition on Software Verification
Autoři
DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T.
Rok RIV
2012
Vydáno
24. 3. 2012
ISSN
0302-9743
Periodikum
Lecture Notes in Computer Science
Ročník
2012
Číslo
7214
Stát
Spolková republika Německo
Strany od
544
Strany do
547
Strany počet
4
URL
BibTex
@article{BUT91458,
author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
title="Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)",
journal="Lecture Notes in Computer Science",
year="2012",
volume="2012",
number="7214",
pages="544--547",
issn="0302-9743",
url="http://www.springerlink.com/content/5x4748456031r18x/"
}