Template-based verification of heap-manipulating programs

Malik, Viktor, Hruska, Martin, Schrammel, Peter and Vojnar, Tomas (2018) Template-based verification of heap-manipulating programs. fmcad.18 Formal Methods in Computer-Aided Design 2018, University of Texas, Austin, Texas, Oct 31 - Nov 2, 2018. Published in: Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD 2018) Austin, Texas, USA, October 30 – November 2, 2018. 103-112. Institute of Electrical and Electronics Engineers ISBN 9780983567882

[img] PDF - Accepted Version
Available under License Creative Commons Attribution.

Download (234kB)

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 a program heap based on logical formulae over bit-vectors. It is based on 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 straight-forward 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 reachability and memory safety properties of programs manipulating dynamic data structures, mainly linked lists. The solution has been implemented in 2LS 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.

Item Type: Conference Proceedings
Keywords: program analysis shape analysis template-based invariant synthesis abstract interpretation SAT/SMT solving
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science > QA0076 Computer software
Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Peter Schrammel
Date Deposited: 24 Aug 2018 14:43
Last Modified: 21 Jan 2019 17:26
URI: http://sro.sussex.ac.uk/id/eprint/78280

View download statistics for this item

📧 Request an update