Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings
Abstract elided by the publisher.
Related papers
- Dynamic partial order reduction for relaxed memory models PLDI 2015
- Formal verification of practical MPI programs PPoPP 2009
- A lock-free relaxed concurrent queue for fast work distribution PPoPP 2021
- Maximal causality reduction for TSO and PSO OOPSLA 2016
- Relaxed Visibility Enhances Partial Order Reduction CAV 1997
- Learning to Split: A Reinforcement-Learning-Guided Splitting Heuristic for Neural Network Verification (Invited Talk) CAV 2026
- Mopsa-C: Improved Verification for C Programs, Simple Validation of Correctness Witnesses (Competition Contribution) TACAS 2024
- Verifying Lock-Free Traversals in Relaxed Memory Separation Logic PLDI 2025