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

axioms and rules of inferencecorrectness of programsshared variablessynchronization

Mathematics Subject Classification ID

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

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

(21)

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

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)