Detail publikačního výsledku

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

Druh

Článek recenzovaný mimo WoS a Scopus

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.

Klíčová slova

separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists

Klíčová slova v angličtině

separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists

Autoři

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

Rok RIV

2012

Vydáno

16.07.2011

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

2011

Číslo

6806

Stát

Spolková republika Německo

Strany od

372

Strany do

378

Strany počet

6

URL

http://www.springerlink.com/content/0348r4140k031426/

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",
  journal="Lecture Notes in Computer Science",
  year="2011",
  volume="2011",
  number="6806",
  pages="372--378",
  issn="0302-9743",
  url="http://www.springerlink.com/content/0348r4140k031426/"
}