🚀 go-pugleaf

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