Scholarlink

This paper introduces a general semantic approach to the definition and formal justification (soundness and completeness) of the Owicki/Gries method for proving correctness of parallel programs. Instantiating the general semantic approach allows to obtain sound and complete proof methods for both the standard model of shared variable concurrency and the concurrency model based on dynamically allocated variables, as described by separation logic.

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

Beyond Concurrent Separation Logic: Who is Afraid of Completeness Proofs?

  • 章节

  • 发表日期：

    2026年

查看全文
  • Frank S. de Boer,
  • Hans-Dieter A. Hiep

摘要

This paper introduces a general semantic approach to the definition and formal justification (soundness and completeness) of the Owicki/Gries method for proving correctness of parallel programs. Instantiating the general semantic approach allows to obtain sound and complete proof methods for both the standard model of shared variable concurrency and the concurrency model based on dynamically allocated variables, as described by separation logic.