Detail publikace

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

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

Originální název

Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

Predator is a tool for automated formal verification of sequential C programs operating with pointers and linked lists. The core algorithms of Predator were originally inspired by works on separation logic with higher-order list predicates, but they are now purely graph-based and significantly extended to support various forms of low-level memory manipulation used in system-level code. This paper briefly introduces Predator and describes its participation in the Software Verification Competition SV-COMP'13 held at TACAS'13.

Klíčová slova

dynamic linked data structuresseparation logic symbolic memory graphslist manipulationlow-level memory manipulationmemory safetyshape analysis

Autoři

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

Rok RIV

2013

Vydáno

17. 3. 2013

Nakladatel

Springer Verlag

Místo

Berlin

ISBN

978-3-642-36742-7

Kniha

Tools and Algorithms for the Construction and Analysis of Systems

Edice

Lecture Notes in Computer Science Volume 7795

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

2013

Číslo

7795

Stát

Spolková republika Německo

Strany od

627

Strany do

629

Strany počet

3

URL

http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49

BibTex

@inproceedings{BUT103454,
  author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  year="2013",
  series="Lecture Notes in Computer Science Volume 7795",
  journal="Lecture Notes in Computer Science",
  volume="2013",
  number="7795",
  pages="627--629",
  publisher="Springer Verlag",
  address="Berlin",
  isbn="978-3-642-36742-7",
  issn="0302-9743",
  url="http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49"
}