Software Verification for Weak Memory via Program Transformation

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

Mathematics Subject Classification ID

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

• Threader
• Checkfence
• PostgreSQL

This page was built for publication: Software Verification for Weak Memory via Program Transformation