Detail publikace

Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic

DUDKA, K. PERINGER, P. VOJNAR, T.

Originální název

Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic

Anglický název

Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic

Jazyk

en

Originální abstrakt

Predator is a new open source tool for verification of sequential C programs with dynamic linked data structures. The tool is conceptually based on separation logic with inductive predicates despite it uses a graph description of heaps. Predator currently handles various forms of lists, including singly-linked as well as doubly-linked lists that may be circular, hierarchically nested and that may have various additional pointer links. Predator is implemented as a gcc plug-in and it is capable of handling lists in the form they appear in real system code, especially the Linux kernel, including a limited support of pointer arithmetic. Collaboration on further development of Predator is welcome.

Anglický abstrakt

Predator is a new open source tool for verification of sequential C programs with dynamic linked data structures. The tool is conceptually based on separation logic with inductive predicates despite it uses a graph description of heaps. Predator currently handles various forms of lists, including singly-linked as well as doubly-linked lists that may be circular, hierarchically nested and that may have various additional pointer links. Predator is implemented as a gcc plug-in and it is capable of handling lists in the form they appear in real system code, especially the Linux kernel, including a limited support of pointer arithmetic. Collaboration on further development of Predator is welcome.

Dokumenty

BibTex


@article{BUT76288,
  author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic",
  annote="Predator is a new open source tool for verification of sequential C programs with
dynamic linked data structures. The tool is conceptually based on separation
logic with inductive predicates despite it uses a graph description of heaps.
Predator currently handles various forms of lists, including singly-linked as
well as doubly-linked lists that may be circular, hierarchically nested and that
may have various additional pointer links. Predator is implemented as a gcc
plug-in and it is capable of handling lists in the form they appear in real
system code, especially the Linux kernel, including a limited support of pointer
arithmetic. Collaboration on further development of Predator is welcome.",
  address="NEUVEDEN",
  chapter="76288",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="6806",
  volume="2011",
  year="2011",
  month="july",
  pages="372--378",
  publisher="NEUVEDEN",
  type="journal article - other"
}