Detail výsledku
Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic
Peringer Petr, Dr. Ing., UITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
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.
separation logic, shape analysis, dynamic linked data structures, pointers, linked lists, tool support, formal verification, Linux lists
@misc{BUT192766,
author="Kamil {Dudka} and Petr {Peringer} and Tomáš {Vojnar}",
title="Predator: A Practical Tool for Checking Manipulation of Dynamic Data Structures Using Separation Logic",
year="2011",
pages="23",
publisher="Faculty of Information Technology BUT",
address="FIT-TR-2011-02, Brno",
url="http://www.fit.vutbr.cz/research/groups/verifit/tools/predator/FIT-TR-2011-02.pdf"
}Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení