Software Verification for Weak Memory via Program Transformation
From MaRDI portal
Publication:5326305
DOI10.1007/978-3-642-37036-6_28zbMath1381.68143arXiv1207.7264OpenAlexW1877513498MaRDI QIDQ5326305
Michael Tautschnig, Jade Alglave, Daniel Kroening, Vincent Nimal
Publication date: 5 August 2013
Published in: Programming Languages and Systems (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1207.7264
Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Mathematical problems of computer architecture (68M07)
Related Items (18)
Integrating Owicki-Gries for C11-style memory models into Isabelle/HOL ⋮ Unifying Operational Weak Memory Verification: An Axiomatic Approach ⋮ Verification of Concurrent Programs on Weak Memory Models ⋮ Unnamed Item ⋮ Stateless model checking for TSO and PSO ⋮ Parallelized sequential composition and hardware weak memory models ⋮ On the van der Waerden numbers \(\mathrm{w}(2; 3, t)\) ⋮ Parameterized model checking on the TSO weak memory model ⋮ Verification of concurrent programs using Petri net unfoldings ⋮ Finding Effective SAT Partitionings Via Black-Box Optimization ⋮ Effective abstractions for verification under relaxed memory models ⋮ Ranking function synthesis for bit-vector relations ⋮ Context-Bounded Analysis of TSO Systems ⋮ Unnamed Item ⋮ Dynamic symbolic verification of MPI programs ⋮ CCA-Secure Keyed-Fully Homomorphic Encryption ⋮ Unnamed Item ⋮ Operational semantics with semicommutations
Uses Software
This page was built for publication: Software Verification for Weak Memory via Program Transformation
