Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] program verification using denotational semantics

Email Gateway (Aug 22 2022 at 12:32):

From: Buday Gergely <gbuday@karolyrobert.hu>
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

Last updated: Apr 23 2024 at 16:19 UTC