Automatic Non-Interference Lemmas for Parameterized Model Checking

13 years 4 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
Authors Jesse D. Bingham
Comments (0)