• Calendar

January 23, Tuesday
12:00 – 14:00

Verification of safety (e.g., invariance) and liveness (e.g., termination) properties of sequential and concurrent systems has traditionally required significant manual effort. For the case of safety, the method of predicate abstraction, suggested by Graf and Saidi, has become a popular semi-manual solution. However, it is generally too weak to deal with liveness. This talk presents a method known as Ranking Abstraction, which is based on program instrumentation, predicate abstraction, and model checking. The method applies the lessons learned from predicate abstraction to the verification of liveness properties. It is then shown that, just like predicate abstraction, the method can be embedded in an refinement process, resulting in a fully automatic method. Time permitting, I will then show how the method is applied to Shape Analysis, i.e., analysis of programs that destructively manipulate heaps. Joint work with Amir Pnueli and Lenore Zuck.