Patrick Cousot (École Normale Supérieure, Paris, F)
Title: Proving Program Invariance and Termination by Parametric Abstraction, Lagrangian Relaxation and Semidefinite Programming
Abstract: In order to verify semialgebraic programs, we automatize the Floyd/Naur/Hoare proof method. The main task is to automatically infer valid invariants and rank functions.
First we express the program semantics in polynomial form. Then the unknown rank function and invariants are abstracted in parametric form. The implication in the Floyd/Naur/Hoare verification conditions is handled by abstraction into numerical constraints by Lagrangian relaxation. The remaining universal quantification is handled by semidefinite programming relaxation. Finally the parameters are computed using semidefinite programming solvers.
This new approach exploits the recent progress in the numerical resolution of linear or bilinear matrix inequalities by semidefinite programming using efficient polynomial primal/dual interior point methods generalizing those well-known in linear programming to convex optimization.
The framework is applied to invariance and termination proof of sequential, nondeterministic, concurrent, and fair parallel imperative polynomial programs and can easily be extended to other safety and liveness properties.
C.A.R. Hoare (Microsoft Research, Cambridge, UK)
Title: The Verifying Compiler, a Grand Challenge for Computing Research
Abstract: The ideas of program verification date back to Turing and von Neumann, who introduced the concept of an assertion as the specification of an interface between parts of a program. The idea of mechanical theorem proving dates back to Leibniz; it has been explored in practice on modern computers by McCarthy, Milner, and many others since. A proposal for 'a program verifier', combining these two technologies, was the subject of a Doctoral dissertation by James C. King, submitted at the Carnegie Institute of Technology in 1969.
Early attempts at automatic program verification were premature. But much progress has been made in the last thirty five years, both in hardware capacity and in the software technologies for verification. I suggest that the renewed challenge of an automatic verifying compiler could provide a focus for interaction, cross-fertilisation, advancement and experimental evaluation of all the technologies of interest in this conference.
Perhaps by concerted international effort, we may be able to meet this challenge, only fifty years after it was proposed by Jim King. We only have fifteen years left to do it.
Amir Pnueli (New York University, USA & Weizmann Institute of Science, IL)
Title: Abstraction for Liveness
Abstract: Unlike model checking which is restricted to finite-state systems, there are two methods which can be applied for the verification of arbitrary infinite-state systems. These are the methods of deductive verification and finitary abstraction (FA). Finitary abstraction is the process which provides an abstraction mapping, mapping a potentially infinite-state system into a finite-state one. After obtaining the finite-state abstraction, we may apply model checking in order to verify the property.
In the talk, we will explore some of the relations between the methods of finitary abstraction and deductive verification. One important connection is the recent proof that finitary abstraction is as powerful as deductive verification, thus establishing the completeness (and universality) of the finitary abstraction method. In order to obtain this result, it was necessary to extend the procedure by allowing augmentation of the verified system with auxiliary variables prior to the application of abstraction. With this extension, it is possible to transform the phenomenon of well-founded descent which is essential for proofs of liveness properties into fairness properties of the finite abstracted system.
Since the proof of completeness of the FA method builds upon the proof of completeness of deductive verification, one may get the false impression that, while being as powerful as deductive verification, FA is not much easier to apply. The focus of the talk is aimed at dispelling this false impression, in particular for the case of liveness properties.
We consider first the case of predicate abstraction, which is a special case of FA. We can view predicate abstraction as an effort to find an inductive assertion, where the user does not know the full form of the assertion but can identify a set of atomic formulas under the conjecture that there exists a useful inductive assertion which is some boolean combination of these atomic formulas. In this case, we let the model checker find for us the correct (and best) boolean combination that yields an inductive assertion. In analogy with this view, we will consider the ``augmented finitary abstraction'' approach as a situation that the user finds it difficult to formulate a full ranking function, as required by deductive verification, but can identify some components of such a ranking function. In that case, we let the model checker arrange and combine these components into a full liveness proof. In both cases, the method relies on the superior ability of model checkers to exhaustively analyze all the combinations of a finite (but possibly large) set of components.
This is work is based on collaboration with Ittai Balaban, Yonit Kesten, and Lenore Zuck.
Contact: RadhiaCousotpolytechnique fr
Last modified: Sunday May 23, 2010 |