Welcome to the new version of CaltechAUTHORS. Login is currently restricted to library staff. If you notice any issues, please email coda@library.caltech.edu
Published May 14, 2001 | Submitted
Report Open

Using Triples to Reason About Concurrent Programs

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
Files (1.8 MB)
Name Size Download all
md5:58adcd22d7e5ded1fb325aae85e778b3
808.9 kB Preview Download
md5:325a5a3ffad9e3be17ccfca3a484740b
959.0 kB Download

Additional details

Created:
August 20, 2023
Modified:
January 13, 2024