Simulation refinement for concurrency verification

DOI10.1016/j.scico.2009.09.006zbMath1220.68069OpenAlexW2017337059MaRDI QIDQ541209

Wim H. Hesselink

Publication date: 6 June 2011

Published in: Science of Computer Programming (Search for Journal in Brave)

Full work available at URL: https://pure.rug.nl/ws/files/2542927/2011SciComputProgHesselink2.pdf

zbMATH Keywords

verificationsimulationrefinementatomicitysemantic completeness

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Uses Software

• NQTHM
• UNITY

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The existence of refinement mappings
• A criterion for atomicity revisited
• A queue based mutual exclusion algorithm
• A state-based approach to communicating processes
• Circumscription - a form of non-monotonic reasoning
• A calculus of communicating systems
• Critique of the Lake Arrowhead three
• Processes are in the eye of the beholder
• Using eternity variables to specify and prove a serializable database interface
• Forward and backward simulations. I. Untimed Systems
• Universal extensions to simulate specifications
• A challenge for atomicity verification
• Splitting forward simulations to cope with liveness
• Refinement verification of the lazy caching algorithm
• Liveness-preserving simulation relations
• Programs, Recursion and Unbounded Choice
• Reduction
• Three logics for branching bisimulation
• Branching time and abstraction in bisimulation semantics
• A theory of normed simulations
• Eternity variables to prove simulation of specifications
• Simulation Refinement for Concurrency Verification
• Completeness of ASM Refinement
• Correct Hardware Design and Verification Methods

This page was built for publication: Simulation refinement for concurrency verification