TY - CONF AB - 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. AU - Kragl, Bernhard AU - Qadeer, Shaz AU - Henzinger, Thomas A ID - 8195 SN - 0302-9743 T2 - Computer Aided Verification TI - Refinement for structured concurrent programs VL - 12224 ER -