Simulation Refinement for Concurrency Verification

DOI10.1016/J.ENTCS.2008.06.002MaRDI QIDQ5403461zbMATH OpenOpenAlexFDO

Authors W. H. Hesselink

Publication date 26 March 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.06.002

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)

Recommendations

• Simulation refinement for concurrency verification
• Verifying concurrent data structures by simulation
• Verification of fine-grain concurrent programs
• Specification and verification of concurrent programs through refinements
• Verification of concurrent systems with VerCors
• Concurrency based transition refinement for the verification of distributed algorithms
• Verifying optimizations for concurrent programs
• Verifying Concurrent Systems with Symbolic Execution

Cites work

• scientific article; zbMATH DE number 3943003 (Why is no real title available?)
• scientific article; zbMATH DE number 193479 (Why is no real title available?)
• A challenge for atomicity verification
• A criterion for atomicity revisited
• A general lock-free algorithm using compare-and-swap
• An assertional proof for a construction of an atomic variable
• Computer Aided Verification
• Eternity variables to prove simulation of specifications
• Forward and backward simulations. I. Untimed Systems
• Lock-free parallel and concurrent garbage collection by mark\&sweep
• On interprocess communication. II: Algorithms
• Reduction
• Refinement verification of the lazy caching algorithm
• Splitting forward simulations to cope with liveness
• The existence of refinement mappings
• Universal extensions to simulate specifications
• Using eternity variables to specify and prove a serializable database interface

Cited in

(7)

• Universal extensions to simulate specifications
• Guarded operations, refinement and simulation
• scientific article; zbMATH DE number 1951183 (Why is no real title available?)
• Simulation refinement for concurrency verification
• Refinement checking based on simulation relations
• Proving refinement using transduction
• Simulation-Based Concurrent Non-malleable Commitments and Decommitments

Describes a project that uses

Uses Software

• NQTHM

This page was built for publication: Simulation Refinement for Concurrency Verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5403461)