Zohar Manna, Stanford
We discuss the problem of generating invariant assertions for programs. These assertions are of immense help in the verification of computer programs. So far, with a few exceptions, the dominant techniques for invariant generation have all been Propagation-Based Techniques. These techniques use the theory of abstract interpretation along with Propagation algorithms and Widening heuristics. These methods have been the basis of many popular and practical tools over the past two decades.
An alternative approach to the generation of invariants is the use of Constraint-Based Techniques. Historically, these techniques have been studied only in restricted domains like Petri Nets. A recent development involves the use of LP Duality along with linear and non-linear Constraint Solving to translate invariant generation problem into a constraint solving problem. While these techniques seem costly at present, they can potentially generate stronger invariants and are able to exploit the program structure better. In this talk, we explore these methods and analyze their pros and cons over related methods.