Refinement verification of the lazy caching algorithm

DOI10.1007/s00236-006-0020-1zbMath1100.68126OpenAlexW2012041760MaRDI QIDQ2509154

Wim H. Hesselink

Publication date: 18 October 2006

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00236-006-0020-1

Mathematics Subject Classification ID

Nonnumerical algorithms (68W05)

Related Items (5)

Simulation Refinement for Concurrency Verification ⋮ Universal extensions to simulate specifications ⋮ Proving linearizability with temporal logic ⋮ Simulation refinement for concurrency verification ⋮ Splitting forward simulations to cope with liveness

Uses Software

• PVS
• UNITY

Cites Work

• The existence of refinement mappings
• Using eternity variables to specify and prove a serializable database interface
• Forward and backward simulations. I. Untimed Systems
• Universal extensions to simulate specifications
• Splitting forward simulations to cope with liveness
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Refinement verification of the lazy caching algorithm