Anzeige
Erschienen in:
2009 | OriginalPaper | Buchkapitel
On Extending Bounded Proofs to Inductive Proofs
verfasst von : Oded Fuhrmann, Shlomo Hoory
Erschienen in: Computer Aided Verification
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
We propose a method for extending a bounded resolution proof to an unbounded inductive proof. More specifically, given a resolution proof that a state machine beginning at an initial state satisfies some property at cycle
k
, we show that the existence of a
Δ
-invariant cut implies that the property holds for cycles
k
+
Δ
,
k
+ 2
Δ
, etc. We suggest a linear algorithm for identifying such
Δ
-extendible proofs and develop the required theory for covering all cycles by
Δ
-extendible proofs. To expose
Δ
-invariant cuts, we develop an efficient proof manipulation algorithm that rearranges the proof by the natural temporal order. We demonstrate the applicability of our techniques on a few real-life examples.