Verification of Concurrent Programs on Weak Memory Models
From MaRDI portal
Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)
Recommendations
- Program verification under weak memory consistency using separation logic
- scientific article; zbMATH DE number 1903349
- On the verification problem for weak memory models
- A wide-spectrum language for verification of programs on weak memory models
- Verification of fine-grain concurrent programs
- Automating deductive verification for weak-memory programs
- A framework for correctness criteria on weak memory models
- Effective Program Verification for Relaxed Memory Models
- Unifying Operational Weak Memory Verification: An Axiomatic Approach
Cites work
- A calculus of communicating systems
- A new solution of Dijkstra's concurrent programming problem
- Counter-Example Guided Fence Insertion under TSO
- Effective Abstractions for Verification under Relaxed Memory Models
- Effective Program Verification for Relaxed Memory Models
- From total store order to sequential consistency: a practical reduction theorem
- How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
- Myths about the mutual exclusion problem
- Software verification for weak memory via program transformation
- Sound and complete monitoring of sequential consistency for relaxed memory models
- Stateless model checking for TSO and PSO
- Thread scheduling for multiprogrammed multiprocessors
- Transactional mutex locks
Cited in
(24)- Cubicle-\(\mathcal{W}\): parameterized model checking on weak memory
- A wide-spectrum language for verification of programs on weak memory models
- Information-flow control on ARM and POWER multicore processors
- Program verification under weak memory consistency using separation logic
- Parameterized model checking on the TSO weak memory model
- Memory model sensitive bytecode verification
- scientific article; zbMATH DE number 1617288 (Why is no real title available?)
- CCA-secure keyed-fully homomorphic encryption
- On Partial Order Semantics for SAT/SMT-Based Symbolic Encodings of Weak Memory Concurrency
- Concurrent Library Correctness on the TSO Memory Model
- A load-buffer semantics for total store ordering
- Owicki-Gries reasoning for weak memory models
- scientific article; zbMATH DE number 522852 (Why is no real title available?)
- An Observational Approach to Defining Linearizability on Weak Memory Models
- Effective Abstractions for Verification under Relaxed Memory Models
- On the verification problem for weak memory models
- Software verification for weak memory via program transformation
- CompCertTSO
- Parallelized sequential composition and hardware weak memory models
- A fine-grained semantics for arrays and pointers under weak memory models
- Overcoming memory weakness with unified fairness. Systematic verification of liveness in weak memory models
- Verifying correctness of persistent concurrent data structures
- Value-dependent information-flow security on weak memory models
- An ACL2 mechanization of an axiomatic framework for weak memory
This page was built for publication: Verification of Concurrent Programs on Weak Memory Models
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3179387)
