Local proofs for global safety properties |
| |
Authors: | Ariel Cohen Kedar S Namjoshi |
| |
Affiliation: | (1) New York University, Courant Institute, 251 Mercer Street, New York, NY 10012, USA;(2) Bell Labs, Room 2B-435, 600-700 Mountain Avenue, Murray Hill, NJ 07974, USA |
| |
Abstract: | This paper explores locality in proofs of global safety properties of concurrent 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 desired global safety property. Local proofs can be more compact than global proofs, but local reasoning
is also inherently incomplete. In this paper, we present an algorithm for safety verification that combines local reasoning
with gradual refinement. The algorithm gradually exposes facts about the internal state of components, until either a local
proof or a real error is discovered. The refinement mechanism ensures completeness. Experiments show that local reasoning
can have significantly better performance over the traditional reachability computation. Moreover, for some parameterized
protocols, a local proof can be used as the basis of a correctness proof over all instances. |
| |
Keywords: | Model checking Local reasoning Compositionality Local proofs |
本文献已被 SpringerLink 等数据库收录! |
|