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:
Article
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
_version_ 1783559638340337664
author Kragl, Bernhard
Qadeer, Shaz
Henzinger, Thomas A.
author_facet Kragl, Bernhard
Qadeer, Shaz
Henzinger, Thomas A.
author_sort Kragl, Bernhard
collection PubMed
description 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.
format Online
Article
Text
id pubmed-7363273
institution National Center for Biotechnology Information
language English
publishDate 2020
record_format MEDLINE/PubMed
spelling pubmed-73632732020-07-16 Refinement for Structured Concurrent Programs Kragl, Bernhard Qadeer, Shaz Henzinger, Thomas A. Computer Aided Verification Article 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. 2020-06-13 /pmc/articles/PMC7363273/ http://dx.doi.org/10.1007/978-3-030-53288-8_14 Text en © The Author(s) 2020 Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made. The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
spellingShingle Article
Kragl, Bernhard
Qadeer, Shaz
Henzinger, Thomas A.
Refinement for Structured Concurrent Programs
title Refinement for Structured Concurrent Programs
title_full Refinement for Structured Concurrent Programs
title_fullStr Refinement for Structured Concurrent Programs
title_full_unstemmed Refinement for Structured Concurrent Programs
title_short Refinement for Structured Concurrent Programs
title_sort refinement for structured concurrent programs
topic Article
url https://www.ncbi.nlm.nih.gov/pmc/articles/PMC7363273/
http://dx.doi.org/10.1007/978-3-030-53288-8_14
work_keys_str_mv AT kraglbernhard refinementforstructuredconcurrentprograms
AT qadeershaz refinementforstructuredconcurrentprograms
AT henzingerthomasa refinementforstructuredconcurrentprograms

Ejemplares similares