[isabelle] program verification using denotational semantics



Hi,

is there extensive literature on using denotational semantics for program verification?

With a quick search I have found

Wolfgang Polak. Program verification based on denotational semantics. In Conference Record of the Eighth ACM Symposium on Principles of Programming Languages, pages 149-158. ACM, January 1981.

http://www.pocs.com/Papers/POPL-81.pdf

and

The Foundations of Program Verification, 2nd Edition Jacques Loeckx, Kurt Sieber
ISBN: 978-0-471-91282-8

and this course:

https://moves.rwth-aachen.de/teaching/ss-15/sv-sw/

Also, is there a practical program verification tool for some language using denotational semantics?

- Gergely




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.