A proof technique for parallel programs

DOI10.1016/0304-3975(84)90122-1zbMATH Open0543.68010OpenAlexW2048147294MaRDI QIDQ796292FDOQ796292

Authors: 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

Recommendations

• scientific article; zbMATH DE number 3907747
• scientific article; zbMATH DE number 3902009
• scientific article; zbMATH DE number 756078
• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• A survey of verification techniques for parallel programs

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)

Cites Work

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

Cited In (17)

• A proof system for a PGAS language
• A simple proof technique for priority-scheduled systems
• Title not available (Why is that?)
• Title not available (Why is that?)
• Observable behavior of dynamic systems: component reasoning for concurrent objects
• Title not available (Why is that?)
• Compositional reasoning about active objects with shared futures
• A sound and complete reasoning system for asynchronous communication with shared futures
• A proof of the correctness of parallel addition to a shared variable in IPCL
• An implementation of mutual inclusion
• Checking sequential correctness in shared-memory parallel programs
• Axiomatic treatment of processes with shared variables revisited
• Observable behavior of distributed systems: component reasoning for concurrent objects
• A generalization of Owicki-Gries's Hoare logic for a concurrent while language
• An introduction to compositional methods for concurrency and their application to real-time.
• A complete axiomatic semantics of spawning
• Key-ABS: a deductive verification tool for the concurrent modelling language ABS

This page was built for publication: A proof technique for parallel programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q796292)