Andreas Lundblad

Verification Condition Generation and Discharge in a Hoare Logic with Recursion

Abstract

The standard approach to automated, Hoare-style program verification is to combine a weakest precondition calculus with a first order logic theorem prover. The calculus either needs explicit loop invariant annotations, or else an additional facility for loop invariant generation.

The alternative scheme we present in this thesis is to use a weakest precondition calculus which produces assertions in a richer language, which does not require loop invariant annotation or generation, but instead a more powerful theorem prover.

The main task of the thesis has been to investigate this approach and to evaluate its effectiveness on concrete examples. Experience from the prototype tool developed show that the approach has a few advantages but requires more research before it can solve any real interesting problems.

Referat

Den vanliga ansatsen till automatiserad, Hoare baserad programverifiering är att kombinera en svagaste förvillkor-kalkyl med en teorembevisare för första ordningens logik. Kalkylen behöver antingen explicita annoteringar för loop-invarianter eller någon facilitet för att generera sådana.

Den alternativa ansatsen vi presenterar här använder en svagaste förvillkor-kalkyl som producerar försäkringar i en rikare logik, vilken inte behöver någon annotering eller generering av loop-invarianter, men istället en mer kraftfull teorembevisare.

Huvuduppgiften i denna uppsats har varit att utforska denna ansats och evaluera dess efektivitet på konkreta exempel. Erfarenhet från prototypverktyget visar att ansatsen har några fördelar med behöver mer utforskning för att kunna lösa några riktigt intressanta problem.