Abstraction Methods for Liveness

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. In this talk we will present an abstraction approach called “ranking abstraction” which is sound and complete for verifying all temporally specified properties, including all liveness properties.

We will start by presenting a general simple framework for state abstraction emphasizing that, in order to get soundness, it is necessary to apply an over-approximating abstraction to the system and an under-approximating abstraction to the (temporal) property. We show that finitary version of this abstraction are complete for verifying all safety properties.

We then consider abstraction approaches to the verification of deadlock freedom, presenting some sufficient conditions guaranteeing that deadlock freedom is inherited from the concrete to the abstract.

Finally, we introduce the method of ranking abstraction and illustrate its application to the verification of termination and more general liveness properties. In this presentation we emphasize the similarity between predicate abstraction and its extension into ranking abstraction. In particular, we illustrate how abstraction refinement can be applied to ranking abstraction. Time permitting, we will present a brief comparison between ranking abstraction and the methods of transition abstraction developed by Podelski, Rybalchenko, and Cook which underly the “Terminator” system.

Speaker Details

Prof. Pnueli is mainly known for the introduction of temporal logic into Computer Science; his work on the application of temporal logic and similar formalisms for the specification and verification of reactive systems; the identification of the class of “Reactive Systems” as systems whose formal specification, analysis, and verification require a distinctive approach; and the development of a rich and detailed methodology, based on temporal logic, for the formal treatment of reactive system; extending this methodology into the realm of real-time systems; and more recently, introducing into formal analysis the models of hybrid systems with appropriate extension of the temporal-logic based methodology.Beside his more theoretical work, concerning a complete axiom system and proof theory for program verification by temporal logic, he also contributed to algorithmic research in this area. He developed a deductive system for linear-time temporal logic and model-checking algorithms for the verification of temporal properties of finite-state systems. Together with David Harel, Pnueli worked on the semantics and implementation of Statecharts, a visual language for the specification, modeling, and prototyping of reactive systems. This language has been applied to avionics, transport, and electronic hardware systems. His current research interests involve synthesis of reactive modules, automatic verification of multi-process systems, and specification methods that combine transition systems with temporal logic. Prof. Pnueli is the 1996 recipient of the ACM Turing award “For his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification”. In 2007, he was nominated as an ACM fellow. Since 1999, Pnueli has been a Professor of Computer Science at the Courant Institute of Mathematical Sciences at New York University.

Date:
Speakers:
Amir Pnueli
Affiliation:
New York University