Publication
Simulation refinement for concurrency verification
Hesselink, 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) [1] 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.
| Original language | English |
|---|---|
| Pages (from-to) | 739-755 |
| Number of pages | 17 |
| Journal | Science of computer programming |
| Volume | 76 |
| Issue number | 9 |
| Publication status | Published - 1-Sep-2011 |
| Event | 13th Refinement Workshop - , Finland Duration: 27-May-2008 → … |
Event
13th Refinement Workshop
27/05/2008 → …
FinlandEvent: Other
- Refinement, Simulation, Atomicity, Verification, Semantic completeness, BRANCHING TIME, SYSTEMS, BISIMULATION, REDUCTION, ALGORITHM, TLA
Keywords
Download statistics
ID: 2542925