Effective Program Verification for Relaxed Memory Models
From MaRDI portal
Publication:3512487
DOI10.1007/978-3-540-70545-1_12zbMath1155.68428OpenAlexW2105980774MaRDI QIDQ3512487
Madanlal Musuvathi, Sebastian Burckhardt
Publication date: 15 July 2008
Published in: Computer Aided Verification (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-540-70545-1_12
Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Related Items (14)
Model Checking Concurrent Programs ⋮ Verification of Concurrent Programs on Weak Memory Models ⋮ Stateless model checking for TSO and PSO ⋮ A formal hierarchy of weak memory models ⋮ Verification of STM on relaxed memory models ⋮ Fences in weak memory models ⋮ Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models ⋮ Deciding Robustness against Total Store Ordering ⋮ Effective abstractions for verification under relaxed memory models ⋮ Context-Bounded Analysis of TSO Systems ⋮ Unnamed Item ⋮ An Isabelle/HOL formalisation of the SPARC instruction set architecture and the TSO memory model ⋮ CCA-Secure Keyed-Fully Homomorphic Encryption ⋮ Abstract semantic diffing of evolving concurrent programs
Uses Software
This page was built for publication: Effective Program Verification for Relaxed Memory Models
