这可能会去 cs 或 cstheory 堆栈交换，但我在这里看到了带有正式验证标记的大多数问题。
是否有大量关于使用指称语义进行程序验证的文献？
通过快速搜索，我发现
沃尔夫冈·波拉克。基于指称语义的程序验证。在第八届 ACM 编程语言原则研讨会的会议记录中，第 149-158 页。ACM，1981 年 1 月。
http://www.pocs.com/Papers/POPL-81.pdf
程序验证的基础，第 2 版 Jacques Loeckx，Kurt Sieber ISBN：978-0-471-91282-8
这门课程：
https://moves.rwth-aachen.de/teaching/ss-15/sv-sw/
此外，是否有使用指称语义的某些语言的实用程序验证工具？