Printable Version of this PageHome PageRecent ChangesSearchSign In

[Mar 28]

Hoare-Flyod-Dijkstra's inductive invariant technique requires a loop invariant. And infering a loop invariant automatically is undecidable for a program with infinite states. Although there has been a lot of work to infer loop invariants, but it is still an open problem!

Techniques for inference of loop invariant:
1. Abstract interpretation based static analysis-
Verification of Java Programs using Symbolic Execution and Invariant Generation. Willem Visser. SPIN04

2. Predicate Abstraction-
Predicate Abstraction for Software Verification. Cormac Flanagan. PoPL02

3. Dynamic Technique-
Static verification of dynamically detected program invariants: Integrating Daikon and ESC/Java. Michael Ernst. RV01

Last modified 29 March 2005 at 12:37 am by Saswat Anand