Local Proofs for Global Safety Properties

13 years 5 days ago
Local Proofs for Global Safety Properties
This paper explores the concept of locality in proofs of global safety properties of asynchronously composed, multi-process programs. Model checking on the full state space is often infeasible due to state explosion. A local proof, in contrast, is a collection of per-process invariants, which together imply the global safety property. Local proofs can be compact: but a central problem is that local reasoning is incomplete. In this paper, we present a “completion” algorithm, which gradually exposes facts about the internal state of components, until either a local proof or a real error is discovered. Experiments show that local reasoning can have significantly better performance over a reachability computation. Moreover, for some parameterized protocols, a local proof can be used to show correctness for all instances.
Ariel Cohen 0002, Kedar S. Namjoshi
Added 07 Jun 2010
Updated 07 Jun 2010
Type Conference
Year 2007
Where CAV
Authors Ariel Cohen 0002, Kedar S. Namjoshi
Comments (0)