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 journalArticleAcademicpeer-review

Copy link to clipboard



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 languageEnglish
Pages (from-to)739-755
Number of pages17
JournalScience of computer programming
Issue number9
Publication statusPublished - 1-Sep-2011
Event13th Refinement Workshop - , Finland
Duration: 27-May-2008 → …


13th Refinement Workshop

27/05/2008 → …


Event: Other


  • Refinement, Simulation, Atomicity, Verification, Semantic completeness, BRANCHING TIME, SYSTEMS, BISIMULATION, REDUCTION, ALGORITHM, TLA

Download statistics

No data available

ID: 2542925