Refinement for Structured Concurrent Programs

摘要

This paper presents a foundation for refining concurrent pro-grams with structured control flow. The verification problem is decomposed into subproblems that aid interactive program development, proof reuse, and automation. The formalization in this paper is the basis of a new design and implementation of the CIVL verifier.