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

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

http://www.springerlink.com/content/5x4748456031r18x/

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",
  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/"
}