Scholarlink

We illustrate the sound and complete construction of program logics by abstraction of a relational semantics into the theory of the logic followed by the formal derivation of the proof system. We consider Hoare logic, O’Hearn incorrectness logic and Hoare incorrectness logic formalizing debugging.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

On the Design of Program Logics

  • 章节

  • 发表日期：

    2026年

查看全文
  • Patrick Cousot

摘要

We illustrate the sound and complete construction of program logics by abstraction of a relational semantics into the theory of the logic followed by the formal derivation of the proof system. We consider Hoare logic, O’Hearn incorrectness logic and Hoare incorrectness logic formalizing debugging.