Simulation refinement for concurrency verificationHesselink, W. H., 1-Sep-2011, In : Science of computer programming. 76, 9, p. 739-755 17 p.
Research output: Contribution to journal › Article › Academic › peer-review
In recent years, we applied and extended the theory of Abadi and Lamport (1991)  on the existence of refinement mappings. The present paper presents an overview of our extensions of the theory. For most concepts we provide examples or pointers to case studies where they occurred. The paper presents the results on semantic completeness. It sketches out how the theory is related to the other formalisms in the area. It discusses the tension between semantic completeness and methodological convenience. It concludes with our experience with the theorem provers NQTHM and PVS that were used during these projects. (C) 2009 Elsevier B.V. All rights reserved.
|Number of pages||17|
|Journal||Science of computer programming|
|Publication status||Published - 1-Sep-2011|
|Event||13th Refinement Workshop - , Finland|
Duration: 27-May-2008 → …
13th Refinement Workshop
27/05/2008 → …Finland
- Refinement, Simulation, Atomicity, Verification, Semantic completeness, BRANCHING TIME, SYSTEMS, BISIMULATION, REDUCTION, ALGORITHM, TLA