0

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?

Gergely
  • 6,879
  • 6
  • 25
  • 35
  • 1
    Abstract Interpretation looks at programs very much from the same viewpoint as denotational semantics does, and in doing so, statically extract properties valid for all inputs. Any static analyzer based on Abstract Interpretation uses a denotational-semantics-like view of the target language and is an answer to the question. – Pascal Cuoq Jan 13 '16 at 14:58
  • Thanks, this is insightful. Still, I am interested in program verification as in using a theorem prover to prove properties of programs. – Gergely Jan 13 '16 at 14:59
  • 1
    Pascal Cuoq makes a good point. Many analyses based on abstract interpretation can be interpreted as running a theorem prover, which however doesn't need (too much) manual input from the user, and tries to prove a property (like never reaching a certain program point, like the location of an overflow etc.). I think you might be interested in this book: http://www.concrete-semantics.org/. It's free, covers all kind of semantics (also the denotational one), and uses Isabelle, a state-of-the art theorem prover. With the help of Isabelle, even OS kernels haven been verified. – Pachelbel Jan 24 '16 at 16:51

0 Answers0