Write a Blog >>

We investigate the decidability of completely automatic program verification for programs that manipulate heaps, and in particular decision procedures for proving memory safety. The work in [Mathur et al. 2019a] identifies decidable sub-classes of uninterpreted programs, but does not address programs that can update functions, which are crucial to model heap-manipulating programs. We develop a new theory of programs, called alias-aware coherent programs, that admits decidable verification. We apply this theory to develop verification algorithms for memory safety— determining if a heap-manipulating program that allocates/frees memory locations and manipulates heap pointers does not dereference a memory location that is not allocated.

We consider this problem when the initial allocated heap forms a forest data-structure (i.e., a disjoint set of trees and lists). While the problem of checking memory safety of programs whose initial heap is a forest data-structure is undecidable, we identify a class of streaming-coherent programs for which the problem is decidable. Our experimental evaluation demonstrates that common library routines that manipulate forest data-structures using a single pass almost always fall in our decidable class. And show that our decision procedure for these programs is effective in both proving memory safety and in identifying memory safety errors.

Presentation slides (POPL20-talk.pptx)2.1MiB

Wed 22 Jan

Displayed time zone: Saskatchewan, Central America change

16:50 - 17:35
Synthesis and Decision ProceduresResearch Papers at Ile de France II (IDF II)
Chair(s): Roopsha Samanta Purdue University
Visualization by Example
Research Papers
Chenglong Wang University of Washington, USA, Yu Feng University of California, Santa Barbara, Rastislav Bodík University of Washington, Alvin Cheung University of California, Berkeley, Işıl Dillig University of Texas Austin
Link to publication DOI Media Attached
Deciding Memory Safety for Single-Pass Heap-Manipulating Programs
Research Papers
Umang Mathur University of Illinois at Urbana-Champaign, Adithya Murali University of Illinois at Urbana-Champaign, Paul Krogmeier University of Illinois at Urbana-Champaign, P. Madhusudan University of Illinois at Urbana-Champaign, Mahesh Viswanathan University of Illinois at Urbana-Champaign
Link to publication DOI Pre-print Media Attached File Attached