University of Sussex
Browse
paper.pdf (228.92 kB)

Template-based verification of heap-manipulating programs

Download (228.92 kB)
conference contribution
posted on 2023-06-09, 14:46 authored by Viktor Malik, Martin Hruska, Peter Schrammel, Tomas Vojnar
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.

History

Publication status

  • Published

File Version

  • Accepted version

Journal

Proceedings of the 18th Conference on Formal Methods in Computer-Aided Design (FMCAD 2018) Austin, Texas, USA, October 30 – November 2, 2018

Publisher

Institute of Electrical and Electronics Engineers

Page range

103-112

Event name

fmcad.18 Formal Methods in Computer-Aided Design 2018

Event location

University of Texas, Austin, Texas

Event type

conference

Event date

Oct 31 - Nov 2, 2018

ISBN

9780983567882

Department affiliated with

  • Informatics Publications

Full text available

  • Yes

Peer reviewed?

  • Yes

Legacy Posted Date

2018-08-24

First Open Access (FOA) Date

2018-08-24

First Compliant Deposit (FCD) Date

2018-08-24

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Licence

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC