Refinement for Structured Concurrent Programs

Bernhard Kragl; Shaz Qadeer; Thomas A. Henzinger

doi:10.1007/978-3-030-53288-8_14

CAV2020顶会

Refinement for Structured Concurrent Programs

Bernhard Kragl, Shaz Qadeer, Thomas A. Henzinger

DOI 出版方

2020年份

10被引次数

6顶会引用

摘要

This paper presents a foundation for refining concurrent programs 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.