A wide-spectrum language for verification of programs on weak memory models

DOI10.1007/978-3-319-95582-7_14zbMath1460.68026arXiv1802.04406OpenAlexW3124453239MaRDI QIDQ2024349

Robert J. Colvin, Graeme Smith

Publication date: 4 May 2021

Full work available at URL: https://arxiv.org/abs/1802.04406

Mathematics Subject Classification ID

Semantics in the theory of computing (68Q55) Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (6)

Information-flow control on ARM and POWER multicore processors ⋮ Trace semantics and algebraic laws for MCA ARMv8 architecture based on UTP ⋮ Parallelized sequential composition and hardware weak memory models ⋮ A wide-spectrum language for verification of programs on weak memory models ⋮ Operational semantics with semicommutations ⋮ Linearizability on hardware weak memory models

Cites Work

• Unnamed Item
• Unnamed Item
• A calculus of communicating systems
• Maude: specification and programming in rewriting logic
• Designing a semantic model for a wide-spectrum language with concurrency
• A wide-spectrum language for verification of programs on weak memory models
• An algebra of synchronous atomic steps
• Tentative steps toward a development method for interfering programs
• Guarded commands, nondeterminacy and formal derivation of programs
• Refinement Calculus
• The specification statement
• A promising semantics for relaxed-memory concurrency

This page was built for publication: A wide-spectrum language for verification of programs on weak memory models