Verification of Concurrent Programs on Weak Memory Models

DOI10.1007/978-3-319-46750-4_1zbMath1482.68147OpenAlexW2521435176MaRDI QIDQ3179387

Oleg Travkin, Heike Wehrheim

Publication date: 21 December 2016

Published in: Theoretical Aspects of Computing – ICTAC 2016 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-319-46750-4_1

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

Parallelized sequential composition and hardware weak memory models ⋮ Unnamed Item ⋮ CCA-Secure Keyed-Fully Homomorphic Encryption

Uses Software

• SPIN
• LLVM
• CBMC
• Checkfence
• UMM
• Lazy-CSeq
• Weak2SC
• GitHub

Cites Work

• A calculus of communicating systems
• Myths about the mutual exclusion problem
• Stateless model checking for TSO and PSO
• Counter-Example Guided Fence Insertion under TSO
• Sound and Complete Monitoring of Sequential Consistency for Relaxed Memory Models
• Transactional Mutex Locks
• Effective Program Verification for Relaxed Memory Models
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• A new solution of Dijkstra's concurrent programming problem
• Effective Abstractions for Verification under Relaxed Memory Models
• Software Verification for Weak Memory via Program Transformation
• From Total Store Order to Sequential Consistency: A Practical Reduction Theorem
• Thread scheduling for multiprogrammed multiprocessors