A proof technique for parallel programs

DOI10.1016/0304-3975(84)90122-1zbMath0543.68010OpenAlexW2048147294MaRDI QIDQ796292

N. Soundararajan

Publication date: 1984

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(84)90122-1

zbMATH Keywords

synchronizationaxioms and rules of inferencecorrectness of programsshared variables

Mathematics Subject Classification ID

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

Related Items

KeY-ABS: A Deductive Verification Tool for the Concurrent Modelling Language ABS ⋮ A generalization of Owicki-Gries's Hoare logic for a concurrent while language ⋮ Compositional reasoning about active objects with shared futures ⋮ Observable behavior of distributed systems: component reasoning for concurrent objects ⋮ A sound and complete reasoning system for asynchronous communication with shared futures ⋮ Axiomatic treatment of processes with shared variables revisited ⋮ An introduction to compositional methods for concurrency and their application to real-time. ⋮ Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects ⋮ A complete axiomatic semantics of spawning

Cites Work

• An axiomatic proof technique for parallel programs
• Verifying properties of parallel programs
• Communicating sequential processes