Mechanized Verification with Sharing

10 years 11 months ago
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...
J. Gregory Malecha, Greg Morrisett
Added 13 Feb 2011
Updated 13 Feb 2011
Type Journal
Year 2010
Authors J. Gregory Malecha, Greg Morrisett
Comments (0)