Result Details

Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)

DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution). Lecture Notes in Computer Science, 2012, vol. 2012, no. 7214, p. 544-547. ISSN: 0302-9743.
Type
journal article
Language
English
Authors
Dudka Kamil, Ing., DITS (FIT)
Müller Petr, Ing., DITS (FIT)
Peringer Petr, Dr. Ing., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

Predator is a tool for automated formal verification of sequential C programs with dynamic linked data structures. It is in principle based on separation logic, but uses a graph-based heap representation. This paper first provides a brief overview of Predator and then discusses experience with its participation in the Software Verification Competition of TACAS'12.

Keywords

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

URL
Published
2012
Pages
544–547
Journal
Lecture Notes in Computer Science, vol. 2012, no. 7214, ISSN 0302-9743
BibTeX 
@article{BUT91458,
  author="Kamil {Dudka} and Petr {Müller} and Petr {Peringer} and Tomáš {Vojnar}",
  title="Predator: A Verification Tool for Programs with Dynamic Linked Data Structures (Competition Contribution)",
  journal="Lecture Notes in Computer Science",
  year="2012",
  volume="2012",
  number="7214",
  pages="544--547",
  issn="0302-9743",
  url="http://www.springerlink.com/content/5x4748456031r18x/"
}
Projects
Advanced secured, reliable and adaptive IT, BUT, Vnitřní projekty VUT, FIT-S-11-1, start: 2011-01-01, end: 2013-12-31, completed
Centrum excelence IT4Innovations, MŠMT, Operační program Výzkum a vývoj pro inovace, ED1.1.00/02.0070, start: 2011-01-01, end: 2015-12-31, completed
Dealing with Complex Data Structures and Concurrency within the Rich Model Toolkit, MŠMT, COST, OC10009, start: 2010-01-01, end: 2012-12-31, running
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness, GACR, Standardní projekty, GAP103/10/0306, start: 2010-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top