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)

Anglický název

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

Jazyk

en

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.

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

Dokumenty

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)",
  annote="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.",
  address="Springer Verlag",
  booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
  chapter="103454",
  edition="Lecture Notes in Computer Science Volume 7795",
  howpublished="print",
  institution="Springer Verlag",
  number="7795",
  year="2013",
  month="march",
  pages="627--629",
  publisher="Springer Verlag",
  type="conference paper"
}