Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
From MaRDI portal
Publication:832723
DOI10.1007/s10817-021-09610-2OpenAlexW3214317778MaRDI QIDQ832723
Brijesh Dongol, Heike Wehrheim, Sadegh Dalvandi, Simon Doherty
Publication date: 25 March 2022
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2004.02983
Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items (2)
Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Reasoning about promises in weak memory models with event structures
Uses Software
Cites Work
- Unnamed Item
- Effective abstractions for verification under relaxed memory models
- Verification of sequential and concurrent programs
- An axiomatic proof technique for parallel programs
- Isabelle. A generic theorem prover
- Stateless model checking for TSO and PSO
- A separation logic for a promising semantics
- Automating deductive verification for weak-memory programs
- Viper: A Verification Infrastructure for Permission-Based Reasoning
- A Program Logic for C11 Memory Fences
- Tackling Real-Life Relaxed Concurrency with FSL++
- Owicki-Gries Reasoning for Weak Memory Models
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Modular Relaxed Dependencies in Weak Memory Concurrency
- Software Verification for Weak Memory via Program Transformation
- Ogre and Pythia: an invariance proof method for weak consistency models
- A promising semantics for relaxed-memory concurrency
- Mathematizing C++ concurrency
- An axiomatic basis for computer programming
- Sledgehammer: Judgement Day
This page was built for publication: Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL
