Faculty of Information Technology, BUT

Publication Details

Template-Based Verification of Heap-Manipulating Programs

HRUŠKA Martin, MALÍK Viktor, SCHRAMMEL Peter and VOJNAR Tomáš. Template-Based Verification of Heap-Manipulating Programs. In: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design. Austin: FMCAD Inc., 2018, pp. 103-111. ISBN 978-0-9835678-8-2. Available from: https://www.cs.utexas.edu/users/hunt/FMCAD/FMCAD18/fmcad2018_proceedings.pdf
Czech title
Verifikace založená na šablonách pro programy pracující s haldou
Type
conference paper
Language
english
Authors
Hruška Martin, Ing. (DITS FIT BUT)
Malík Viktor, Ing. (DITS FIT BUT)
Schrammel Peter, Dr. (US)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords
software analysis, software verification, shape analysis, template based verification, 2LS, love, domain combination
Abstract
We propose a shape analysis suitable for analysis engines that perform automatic invariant inference using an SMT solver. The proposed solution includes an abstract template domain that encodes the shape of the program heap based on logical formulae over bit-vectors. It is based on computing a points-to relation between pointers and symbolic addresses of abstract memory objects. Our abstract heap domain can be combined with value domains in a straightforward manner, which particularly allows us to reason about shapes and contents of heap structures at the same time. The information obtained from the analysis can be used to prove memory safety and reachability properties, expressed by user assertions, of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in the 2LS framework and compared against state-of-the-art tools that perform the best in heap-related categories of the well-known Software Verification Competition (SV-COMP). Results show that 2LS outperforms these tools on benchmarks requiring combined reasoning about unbounded data structures and their numerical contents.
Published
2018
Pages
103-111
Proceedings
Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design
Conference
Formal Methods in Computer-Aided Design, Austin, Texas, US
ISBN
978-0-9835678-8-2
Publisher
FMCAD Inc.
Place
Austin, US
DOI
BibTeX
@INPROCEEDINGS{FITPUB11861,
   author = "Martin Hru\v{s}ka and Viktor Mal\'{i}k and Peter Schrammel and Tom\'{a}\v{s} Vojnar",
   title = "Template-Based Verification of Heap-Manipulating Programs",
   pages = "103--111",
   booktitle = "Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design",
   year = 2018,
   location = "Austin, US",
   publisher = "FMCAD Inc.",
   ISBN = "978-0-9835678-8-2",
   doi = "10.23919/FMCAD.2018.8603009",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/11861"
}
Back to top