-
Patrick Cousot.
Partial Completeness of Abstract Fixpoint Checking.
ROPAS, National Creative Research
Initiatives Center, Dept. of Computer
Science, KAIST, Taejon, Republic of Corea, June 12, 2000.
- Abstract:
Abstract interpretation is used in program static analysis and model
checking to cope with infinite state spaces and/or with computer
resource limitations. One common problem is to check abstract
fixpoints for specifications. The abstraction is \emph{partially
complete} when the checking algorithm is exact in that, if the
algorithm ever terminates, its answer is always affirmative for
correct specifications. We characterize partially complete
abstractions for various abstract fixpoint checking algorithms,
including new ones, and show that the computation of complete abstract
domains is essentially equivalent to invariance proofs that is to
concrete fixpoint checking.
-
Slides of the 2h seminar: .pdf.
- This work was published in SARA'2000.