Refinement for structured concurrent programs

Kragl, Bernhard; Qadeer, Shaz; Henzinger, Thomas A

Refinement for structured concurrent programs

Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.

Download

2020_LNCS_Kragl.pdf 804.24 KB [Published Version]

DOI

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

Conference Paper | Published | English

Scopus indexed

Author

Kragl, Bernhard^ISTA ; Qadeer, Shaz; Henzinger, Thomas A^ISTA

Corresponding author has ISTA affiliation

Department

Henzinger_Thomas Group

Grant

Wittgenstein Award – Thomas Henzinger

Series Title

LNCS

Abstract

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.

Publishing Year

2020

Date Published

2020-07-14

Proceedings Title

Computer Aided Verification

Publisher

Springer Nature

Acknowledgement

Bernhard Kragl and Thomas A. Henzinger were supported by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award).

Volume

12224

Page

275-298

ISBN

9783030532871

ISSN

0302-9743

eISSN

1611-3349

IST-REx-ID

8195

Cite this

Kragl B, Qadeer S, Henzinger TA. Refinement for structured concurrent programs. In: Computer Aided Verification. Vol 12224. Springer Nature; 2020:275-298. doi:10.1007/978-3-030-53288-8_14

Kragl, B., Qadeer, S., & Henzinger, T. A. (2020). Refinement for structured concurrent programs. In Computer Aided Verification (Vol. 12224, pp. 275–298). Springer Nature. https://doi.org/10.1007/978-3-030-53288-8_14

Kragl, Bernhard, Shaz Qadeer, and Thomas A Henzinger. “Refinement for Structured Concurrent Programs.” In Computer Aided Verification, 12224:275–98. Springer Nature, 2020. https://doi.org/10.1007/978-3-030-53288-8_14.

B. Kragl, S. Qadeer, and T. A. Henzinger, “Refinement for structured concurrent programs,” in Computer Aided Verification, 2020, vol. 12224, pp. 275–298.

Kragl B, Qadeer S, Henzinger TA. 2020. Refinement for structured concurrent programs. Computer Aided Verification. , LNCS, vol. 12224, 275–298.

Kragl, Bernhard, et al. “Refinement for Structured Concurrent Programs.” Computer Aided Verification, vol. 12224, Springer Nature, 2020, pp. 275–98, doi:10.1007/978-3-030-53288-8_14.

All files available under the following license(s):

Creative Commons Attribution 4.0 International Public License (CC-BY 4.0):