An approach to automating the verification of compact parallel coordination programs. I

DOI10.1007/BF00289237zbMath0522.68017OpenAlexW2042876806MaRDI QIDQ1056221

Boris D. Lubachevsky

Publication date: 1984

Published in: Acta Informatica (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/bf00289237

zbMATH Keywords

correctness proofcompact parallel programmeta-statesNYU-ultracomputerreachability set descriptionshared memory asynchronous parallel processor

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items (10)

Model checking and abstraction to the aid of parameterized systems (a survey) ⋮ Two algorithms for barrier synchronization ⋮ Mind the Shapes: Abstraction Refinement Via Topology Invariants ⋮ \(\text{Para}^2\): parameterized path reduction, acceleration, and SMT for reachability in threshold-guarded distributed algorithms ⋮ Compositionality Entails Sequentializability ⋮ View abstraction for systems with component identities ⋮ Verifying Parameterized taDOM+ Lock Managers ⋮ On the completeness of bounded model checking for threshold-based distributed algorithms: reachability ⋮ The Spotlight Principle ⋮ Quicker Convergence for Iterative Numerical Solutions to Stochastic Problems: Probabilistic Interpretations, Ordering Heuristics, and Parallel Processing

Cites Work

• Unnamed Item
• Unnamed Item
• The temporal semantics of concurrent programs
• System modelling with high-level Petri nets
• On the reachability problem for 5-dimensional vector addition systems
• Proving assertions about parallel programs
• A starvation-free solution to the mutual exclusion problem
• Parallel program schemata
• A lattice-theoretical fixpoint theorem and its applications
• Synthesis of Resource Invariants for Concurrent Programs
• Proving Liveness Properties of Concurrent Programs
• Verifying properties of parallel programs
• Basic Techniques for the Efficient Coordination of Very Large Numbers of Cooperating Sequential Processors

This page was built for publication: An approach to automating the verification of compact parallel coordination programs. I