Detail publikace

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures

DUDKA, K. MÜLLER, P. PERINGER, P. VOJNAR, T.

Originální název

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures

Anglický název

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures

Jazyk

en

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.

Anglický 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.

Dokumenty

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",
  annote="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.",
  address="NEUVEDEN",
  chapter="91458",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="7214",
  volume="2012",
  year="2012",
  month="march",
  pages="544--547",
  publisher="NEUVEDEN",
  type="journal article - other"
}