CODEWITHSUNDEEP
proofformal-verificationdenotational-semantics
Gergely
Gergely

Reputation: 7487

Formal verification using denotational semantics?

This might go to cs or cstheory stack exchange, but I have seen the most questions tagged with formal-verification here.

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

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?

Upvotes: 0

Views: 142

Answers (0)

Related Questions