Deciding memory safety for single-pass heap-manipulating programs

Umang Mathur, Adithya Murali, Paul Krogmeier, Madhusudan Parthasarathy, Mahesh Viswanathan

Research output: Contribution to journalArticle

Abstract

We investigate the decidability of automatic program verification for programs that manipulate heaps, and in particular, decision procedures for proving memory safety for them. We extend recent work that identified a decidable subclass of uninterpreted programs to a class of alias-aware programs that can update maps. We apply this theory to develop verification algorithms for memory safety - determining if a heap-manipulating program that allocates and frees memory locations and manipulates heap pointers does not dereference an unallocated memory location. We show that this problem is decidable when the initial allocated heap forms a forest data-structure and when programs are streaming-coherent, which intuitively restricts programs to make a single pass over a data-structure. Our experimental evaluation on a set of library routines that manipulate forest data-structures shows that common single-pass algorithms on data-structures often fall in the decidable class, and that our decision procedure is efficient in verifying them.

Original languageEnglish (US)
Article number35
JournalProceedings of the ACM on Programming Languages
Volume4
Issue numberPOPL
DOIs
StatePublished - Jan 2020

Keywords

  • Aliasing
  • Decidability
  • Forest Data-Structures
  • Memory Safety
  • Program Verification
  • Streaming-Coherence
  • Uninterpreted Programs

ASJC Scopus subject areas

  • Software
  • Safety, Risk, Reliability and Quality

Fingerprint Dive into the research topics of 'Deciding memory safety for single-pass heap-manipulating programs'. Together they form a unique fingerprint.

  • Cite this