Result Details
Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution)
DUDKA, K.; MÜLLER, P.; PERINGER, P.; VOJNAR, T. Predator: A Tool for Verification of Low-Level List Manipulation (Competition Contribution). Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science. Lecture Notes in Computer Science Volume 7795. Berlin: Springer Verlag, 2013. no. 7795, p. 627-629. ISBN: 978-3-642-36742-7. ISSN: 0302-9743.
Type
conference paper
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)
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 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.
Keywords
dynamic linked data structures
separation logic
symbolic memory graphs
symbolic memory graphs
list manipulation
low-level memory manipulation
memory safety
shape analysis
URL
Published
2013
Pages
627–629
Journal
Lecture Notes in Computer Science, vol. 2013, no. 7795, ISSN 0302-9743
Proceedings
Tools and Algorithms for the Construction and Analysis of Systems
Series
Lecture Notes in Computer Science Volume 7795
Conference
European Joint Conferences on Theory and Practice of Software -- ETAPS'13 (TACAS'13)
ISBN
978-3-642-36742-7
Publisher
Springer Verlag
Place
Berlin
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)",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2013",
series="Lecture Notes in Computer Science Volume 7795",
journal="Lecture Notes in Computer Science",
volume="2013",
number="7795",
pages="627--629",
publisher="Springer Verlag",
address="Berlin",
isbn="978-3-642-36742-7",
issn="0302-9743",
url="http://link.springer.com/chapter/10.1007/978-3-642-36742-7_49"
}
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
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
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-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
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
Verifikace a optimalizace počítačových systémů, BUT, Vnitřní projekty VUT, FIT-S-12-1, start: 2012-01-01, end: 2014-12-31, completed
Research groups
Departments