Back to Search Start Over

Three Early Formal Approaches to the Verification of Concurrent Programs.

Authors :
Jones, Cliff B.
Source :
Minds & Machines; 2024 Suppl 1, Vol. 34, p73-92, 20p
Publication Year :
2024

Abstract

This paper traces a relatively linear sequence of early research approaches to the formal verification of concurrent programs. It does so forwards and then backwards in time. After briefly outlining the context, the key insights from three distinct approaches from the 1970s are identified (Ashcroft/Manna, Ashcroft (solo) and Owicki). The main technical material in the paper focuses on a specific program taken from the last published of the three pieces of research (Susan Owicki's): her own verification of her Findpos example is outlined followed by attempts at verifying the same example using the earlier approaches. Reconsidering the prior approaches on the basis of Owicki's useful example illuminates similarities and differences between the proposals. Along the way, observations about interactions between researchers (and some "blind spots") are noted. [ABSTRACT FROM AUTHOR]

Subjects

Subjects :
RESEARCH personnel
SHIFT registers

Details

Language :
English
ISSN :
09246495
Volume :
34
Database :
Complementary Index
Journal :
Minds & Machines
Publication Type :
Academic Journal
Accession number :
176119787
Full Text :
https://doi.org/10.1007/s11023-023-09621-5