Published 1993
| Submitted
Technical Report
Open
Using Triples to Reason About Concurrent Programs
- Creators
- Chandy, K. Mani
Chicago
An error occurred while generating the citation.
Abstract
This paper presents adaptations of the Hoare triple for reasoning about concurrent programs. The rules for the Hoare triple, familiar to programmers from their experience with sequential programming, can be applied to develop proofs of concurrent programs as well. The basis for the adaptations of the Hoare triple is temporal logic.
Additional Information
© 1993 California Institute of Technology. Thanks at Caltech to U. Binau, M. van der Goot, P. Hofstee, R. Leino, B. Massingill, A. Rifkin, P. Sivilotti, J. van de Snepscheut, L. Lamport, J. Misra and A. Singh for their careful reading. Special thanks to Rustan Leino for pointing out the identity element and the idempotence of parallel composition, and for strengthening some theorems by replacing implication by equality.Attached Files
Submitted - 93-02.pdf
Submitted - 93-02.ps
Files
93-02.pdf
Additional details
- Eprint ID
- 26855
- Resolver ID
- CaltechCSTR:1993.cs-tr-93-02
- Created
-
2001-05-14Created from EPrint's datestamp field
- Updated
-
2019-10-03Created from EPrint's last_modified field
- Caltech groups
- Computer Science Technical Reports
- Series Name
- Computer Science Technical Reports