4pm Tuesday 7 August 2001
Room 2511, JCMB, King's Buildings
Formal verification of programs is generally accepted to be laborious and time consuming. Even simple examples generate significant syntactic overhead, producing a daunting number of proof obligations. A verification condition generator (VCG) can significantly reduce the amount of work required.
I shall present work on a VCG for the Abadi-Leino logic (AL) of objects that Martin Hofmann and I have been working on recently. Our VCG algorithm involves type inference based on an automaton in the style of Palsberg's previous work, and also instantiation of second-order existential variables, akin to Bledsoe's maximal set method.
Given a program, we construct a skeleton proof, which is fleshed out by providing variables for the unknown components. We read-off the side conditions to give us constraints on these unknowns. By existentially quantifying the unknown (second-order) components we obtain a second-order verification condition (VC). We provide rules that can be applied to automatically instantiate the existentially quantified variables leaving us with a first-order, fix-point VC. The fix-points can be eliminated from the VC by allowing the user/programmer to provide annotations within the input program which induce further constraints on the unknowns.
We have manually applied the algorithm to an annotated incarnation of the gcd algorithm as presented in [Abadi, Leino 97] and obtained a first-order VC that has shed most of the overhead caused by objects, leaving us with the key algorithmic properties of gcd. It is conjectured that this VC can be automatically discharged by an automated theorem prover with some cleverly formulated lemmas. In contrast, the same example attempted using LEGO in [Hofmann, Tang 2000] took three weeks and a resulting proof script of several pages.
(Joint work with Martin Hofmann.)
Martin Grohe
Friday, 20 Juli 2001
An error occured whilst processing this directive