Automating deductive verification for weak-memory programs
From MaRDI portal
Publication:2324213
DOI10.1007/978-3-319-89960-2_11zbMath1423.68111arXiv1703.06368OpenAlexW2605169925MaRDI QIDQ2324213
Alexander J. Summers, Peter Müller
Publication date: 16 September 2019
Full work available at URL: https://arxiv.org/abs/1703.06368
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (5)
Concise Read-Only Specifications for Better Synthesis of Programs with Pointers ⋮ Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Making Linearizability Compositional for Partially Ordered Executions ⋮ Concise outlines for a complex logic: a proof outline checker for TaDA
Uses Software
This page was built for publication: Automating deductive verification for weak-memory programs
