Publication: Automated and modular refinement reasoning for concurrent programs
Program
KU-Authors
KU Authors
Co-Authors
Hawblitzel, Chris
Petrank, Erez
Qadeer, Shaz
Publication Date
Language
Embargo Status
Journal Title
Journal ISSN
Volume Title
Alternative Title
Abstract
We present CIVL, a language and verifier for concurrent programs based on automated and modular refinement reasoning. CIVL supports reasoning about a concurrent program at many levels of abstraction. Atomic actions in a high-level description are refined to fine-grain and optimized lower-level implementations. A novel combination of automata theoretic and logic-based checks is used to verify refinement. Modular specifications and proof annotations, such as location invariants and procedure pre- and post-conditions, are specified separately, independently at each level in terms of the variables visible at that level. We have implemented CIVL as an extension to the BOOGIE language and verifier. We have used CIVL to refine a realistic concurrent garbage collection algorithm from a simple high-level specification down to a highly-concurrent implementation described in terms of individual memory accesses.
Source
Publisher
Springer International Publishing Ag
Subject
Computer science, Software engineering, Computer science-mathematics, Electrical electronics engineering
Citation
Has Part
Source
Computer Aided Verification, Cav 2015, Pt II
Book Series Title
Edition
DOI
10.1007/978-3-319-21668-3_26