Publication:
Automated and modular refinement reasoning for concurrent programs

Placeholder

Departments

School / College / Institute

Program

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

item.page.datauri

Link

Rights

Copyrights Note

Endorsement

Review

Supplemented By

Referenced By

0

Views

0

Downloads

View PlumX Details