Description:
In this Microsoft Research video, Amir Pnueli, professor of Computer Science at New York University, discusses ranking abstraction, an abstraction approach which is sound and complete for verifying all temporally specified properties, including all liveness properties. It is a known fact that finitary state abstraction methods, such as predicate abstraction, are inadequate for verifying general liveness properties or even termination of sequential programs. Thus, this new approach could change the future of abstraction approaches. Learn more about this approach as Professor Pnueli illustrates the application of ranking abstraction to the verification of termination and more general liveness properties, particularly how abstraction refinement can be applied to ranking abstraction.
Speaker(s):
Amir Pnueli, Professor of Computer Science, Courant Institute of Mathematical Sciences, New York University
|
