A proof technique for parallel programs

DOI10.1016/0304-3975(84)90122-1MaRDI QIDQ796292zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(17)

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

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)