Browse by author
Lookup NU author(s): Professor Cliff JonesORCiD
This work is licensed under a Creative Commons Attribution 4.0 International License (CC BY 4.0).
© 2023, The Author(s). 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.
Author(s): Jones CB
Publication type: Article
Publication status: Published
Journal: Minds and Machines
Year: 2024
Volume: 34
Pages: 73–92
Print publication date: 01/02/2024
Online publication date: 23/01/2023
Acceptance date: 03/01/2023
Date deposited: 07/02/2023
ISSN (print): 0924-6495
ISSN (electronic): 1572-8641
Publisher: Springer Science and Business Media B.V.
URL: https://doi.org/10.1007/s11023-023-09621-5
DOI: 10.1007/s11023-023-09621-5
Altmetrics provided by Altmetric
