Mechanized Verification with Sharing

We consider software verification of imperative programs by theorem proving in higher-order separation logic. Of particular interest are the difficulties of encoding and reasoning about sharing and aliasing in pointer-based data structures. Both of these are difficulties for reasoning in separation logic because they rely, fundamentally, on non-separate heaps. We show how sharing can be achieved while preserving abstraction using mechanized reasoning about fractional permissions in Hoare type theory. 1 Motivation Axiomatic semantics [7] is one way to formally reason about programs. Under these semantics, programs are analyzed by considering the effect of primitive operations on predicates over the heap. Unfortunately, stating and reasoning about these predicates is complicated due to potential pointer aliasing. It was not until Reynolds proposed separation logic [16] that reasoning about imperative programs in a modular way became tractable. However, even with this logic some specifica...

• Type: Journal
• Year: 2010
• Where: ICTAC
• Authors: J. Gregory Malecha, Greg Morrisett
• Keywords: Applied Computing, ICTAC 2010, Imperative Programs, Reasoning, Separation Logic