Seeking verification condition generators

Thread View: comp.specification

2 messages

[T] Back to Threads [V] Tree View [G] Group Articles

2 total messages Started by David Sims Mon, 06 Apr 1992 14:42

#51

Author: David Sims
Date: Mon, 06 Apr 1992 14:42

26 lines
1408 bytes

Hello,

I'm looking for software tools or references to papers that address
verification condition generators (program correctness condition
generators).  My literature search to date has come up empty :(

Given a program annotated by axiomatic style verification conditions
(preconditions and postconditions), this tool will extract each
precondition/postcondition pair (possibly using the "weakest precondition"
function) and send it to a theorem prover.  If the theorem prover verifies
all the assertions sent to it by the verification condition generator,
then the program has been proved correct.

Such a tool will avoid reproving assertions that were already proved.  It
might make other optimizations as well.

***

Pointers to references or tools for any programming language would be
greatly appreciated.


Thanks,

David Sims
dsims@thor.ece.uc.edu

Re: Seeking verification condition generators

#52

Author: Jon Jacky
Date: Tue, 07 Apr 1992 16:07

26 lines
1475 bytes

This book describes a solution in Lisp for a Pascal-like language.  In 
addition to the VC generator, it also presents the theorem prover:

@book{gordon88,
        author="Michael J.C. Gordon",
        title="Programming Language Theory and its Implementation: Applicative
                and Imperative Paradigms",
        publisher="Prentice Hall",
        year=1988}

A shorter article on the topic is:

@article{gray87,
        author="D. Gray",
        title="A Pedagogical Verification Condition Generator",
        journal="The Computer Journal",
        volume=30,
        number=3,
        year=1987,
        pages="239 -- 248"}

Jonathan Jacky                      jon@radonc.washington.edu
Radiation Oncology RC-08            (206)-548-4117 voice
University of Washington            (206)-548-6218 fax
Seattle, WA 98195
USA

Thread Navigation

This is a paginated view of messages in the thread with full content displayed inline.

Messages are displayed in chronological order, with the original post highlighted in green.

Use pagination controls to navigate through all messages in large threads.

Back to All Threads