Sciweavers

Share
FMCAD
2008
Springer

Automatic Non-Interference Lemmas for Parameterized Model Checking

9 years 3 months ago
Automatic Non-Interference Lemmas for Parameterized Model Checking
Parameterized model checking refers to any method that extends traditional, finite-state model checking to handle systems arbitrary number of processes. One popular approach to this problem uses abstraction and so-called guard strengthening. Here number of processes remain intact, while the rest are abstracted away. This initially causes counter-examples, but the user e non-interference lemmas, which eliminate spurious behavior by the abstracted processes. The technique is sound in that if the user writes a lemma that is not invariant, the proof will never succeed. Though the non-interference lemmas are typically much simpler than writing a full inductive invariant, there is still a non-trivial amount of human insight needed to analysis counter-examples and concoct the lemmas. In our work, we show how the process of inferring appropriate non-interference lemmas can be automated. oach is based on a very general theory that simply assumes a Galois connection between the concrete and abst...
Jesse D. Bingham
Added 26 Oct 2010
Updated 26 Oct 2010
Type Conference
Year 2008
Where FMCAD
Authors Jesse D. Bingham
Comments (0)
books