Cargando…

Refinement for Structured Concurrent Programs

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 implementati...

Descripción completa

Detalles Bibliográficos
Autores principales: Kragl, Bernhard, Qadeer, Shaz, Henzinger, Thomas A.
Formato: Online Artículo Texto
Lenguaje:English
Publicado: 2020
Materias:
Acceso en línea:https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363273/
http://dx.doi.org/10.1007/978-3-030-53288-8_14
Descripción
Sumario: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.