{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,20]],"date-time":"2026-03-20T08:45:32Z","timestamp":1773996332401,"version":"3.50.1"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"S1","license":[{"start":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T00:00:00Z","timestamp":1674432000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T00:00:00Z","timestamp":1674432000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100000275","name":"Leverhulme Trust","doi-asserted-by":"publisher","award":["RPG-2019-020"],"award-info":[{"award-number":["RPG-2019-020"]}],"id":[{"id":"10.13039\/501100000275","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Minds &amp; Machines"],"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>\n                    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\u2019s): her own verification of her\n                    <jats:italic>Findpos<\/jats:italic>\n                    example is outlined followed by attempts at verifying the same example using the earlier approaches. Reconsidering the prior approaches on the basis of Owicki\u2019s useful example illuminates similarities and differences between the proposals. Along the way, observations about interactions between researchers (and some \u201cblind spots\u201d) are noted.\n                  <\/jats:p>","DOI":"10.1007\/s11023-023-09621-5","type":"journal-article","created":{"date-parts":[[2023,1,23]],"date-time":"2023-01-23T10:02:57Z","timestamp":1674468177000},"page":"73-92","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["Three Early Formal Approaches to the Verification of Concurrent Programs"],"prefix":"10.1007","volume":"34","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0038-6623","authenticated-orcid":false,"given":"Cliff B.","family":"Jones","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2023,1,23]]},"reference":[{"key":"9621_CR1","doi-asserted-by":"crossref","unstructured":"Abrial, J. R. (2010). Modeling in Event-B: System and Software Engineering. Cambridge University Press.","DOI":"10.1017\/CBO9781139195881"},{"key":"9621_CR2","doi-asserted-by":"crossref","unstructured":"Apt, K. R., & Hoare, T. (Eds.). (2022). Edsger Wybe Dijkstra: His life, work and legacy. ACM.","DOI":"10.1145\/3544585"},{"key":"9621_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-4376-0","volume-title":"Verification of sequential and concurrent programs","author":"KR Apt","year":"1991","unstructured":"Apt, K. R., & Olderog, E. R. (1991). Verification of sequential and concurrent programs. Springer."},{"issue":"6","key":"9621_CR4","doi-asserted-by":"publisher","first-page":"751","DOI":"10.1007\/s00165-019-00501-3","volume":"31","author":"KR Apt","year":"2019","unstructured":"Apt, K. R., & Olderog, E. R. (2019). Fifty years of hoare\u2019s logic. Formal Aspects of Computing, 31(6), 751\u2013807.","journal-title":"Formal Aspects of Computing"},{"key":"9621_CR5","unstructured":"Ashcroft, E. A. (1970). Mathematical logic applied to the semantics of computer programs. PhD thesis, University of London."},{"issue":"1","key":"9621_CR6","doi-asserted-by":"publisher","first-page":"110","DOI":"10.1016\/S0022-0000(75)80018-3","volume":"10","author":"EA Ashcroft","year":"1975","unstructured":"Ashcroft, E. A. (1975). Proving assertions about parallel programs. Journal of Computer and System Sciences, 10(1), 110\u2013135.","journal-title":"Journal of Computer and System Sciences"},{"key":"9621_CR7","unstructured":"Ashcroft, E. A., & Manna, Z. (1970). Formalization of properties of parallel programs. Tech. Rep. AIM-110, Stanford Artificial Intelligence Project. https:\/\/apps.dtic.mil\/sti\/citations\/AD0708740. Published as Ashcroft and Manna (1971)"},{"key":"9621_CR8","unstructured":"Ashcroft, E. A., & Manna, Z. (1971). Formalization of properties of parallel programs. In B. Meltzer & D. Michie (Eds.), Machine intelligence (Vol. 6, pp. 17\u201341). Edinburgh University Press."},{"issue":"3","key":"9621_CR9","doi-asserted-by":"publisher","first-page":"336","DOI":"10.1137\/0205029","volume":"5","author":"EA Ashcroft","year":"1976","unstructured":"Ashcroft, E. A., & Wadge, W. W. (1976). Lucid\u2013a formal system for writing and proving programs. SIAM Journal on Computing, 5(3), 336\u2013354.","journal-title":"SIAM Journal on Computing"},{"key":"9621_CR10","unstructured":"Ashcroft, E. A., & Wadge, W. W. (1979). R for semantics. Tech. Rep. CS-79-37, Faculty of Mathematics, University of Waterloo, Canada"},{"key":"9621_CR11","doi-asserted-by":"crossref","unstructured":"Dershowitz, N., & Waldinger, R. (2019). Zohar Manna (1939\u20132018). Formal Aspects of Computing, 31(6), 643\u2013660.","DOI":"10.1007\/s00165-019-00500-4"},{"issue":"8","key":"9621_CR12","doi-asserted-by":"publisher","first-page":"453","DOI":"10.1145\/360933.360975","volume":"18","author":"E Dijkstra","year":"1975","unstructured":"Dijkstra, E. (1975). Guarded commands, non-determinacy, and formal languages. Communications of the ACM, 18(8), 453\u2013457.","journal-title":"Communications of the ACM"},{"key":"9621_CR13","volume-title":"A discipline of programming","author":"EW Dijkstra","year":"1976","unstructured":"Dijkstra, E. W. (1976). A discipline of programming. Prentice Hall."},{"key":"9621_CR14","doi-asserted-by":"crossref","unstructured":"Dijkstra, E. W. (1982). A personal summary of the Gries\u2013Owicki theory. In E. W. Dijkstra (Ed.), Selected writings on computing: A personal perspective. Texts and monographs in computer science. Springer, EWD554.","DOI":"10.1007\/978-1-4612-5695-3_33"},{"key":"9621_CR15","doi-asserted-by":"crossref","unstructured":"Flon, L., & Suzuki, N. (1978). Consistent and complete proof rules for the total correctness of parallel programs. Tech. Rep. CSl-78-6, Xerox, Palo Alto.","DOI":"10.1109\/SFCS.1978.11"},{"key":"9621_CR16","doi-asserted-by":"crossref","unstructured":"Floyd, R. W. (1967). Assigning meanings to programs. In J. Schwartz (Ed.), Mathematical aspects of computer science, Proceedings of symposia in applied mathematics (Vol. 19, pp. 19\u201332). American Mathematical Society.","DOI":"10.1090\/psapm\/019\/0235771"},{"key":"9621_CR17","doi-asserted-by":"crossref","unstructured":"Hayes, I. J., & Jones, C. B. (2018). A guide to rely\/guarantee thinking. Lecture notes in computer scienceIn J. Bowen, Z. Liu, & Z. Zhan (Eds.), Engineering trustworthy software systems\u2014Third International School, SETSS 2017 (Vol. 11174, pp. 1\u201338). Springer.","DOI":"10.1007\/978-3-030-02928-9_1"},{"issue":"10","key":"9621_CR18","doi-asserted-by":"publisher","first-page":"576","DOI":"10.1145\/363235.363259","volume":"12","author":"CAR Hoare","year":"1969","unstructured":"Hoare, C. A. R. (1969). An axiomatic basis for computer programming. Communications of the ACM, 12(10), 576\u2013580.","journal-title":"Communications of the ACM"},{"key":"9621_CR19","doi-asserted-by":"publisher","unstructured":"Hoare, C. A. R. (1971). Proof of a program: FIND. Communications of the ACM, 14(1), 39\u201345. https:\/\/doi.org\/10.1145\/362452.362489","DOI":"10.1145\/362452.362489"},{"key":"9621_CR20","first-page":"61","volume-title":"Operating System Techniques","author":"CAR Hoare","year":"1972","unstructured":"Hoare, C. A. R. (1972). Towards a theory of parallel programming. In C. A. R. Hoare & R. Perrott (Eds.), Operating System Techniques (pp. 61\u201371). Academic Press."},{"key":"9621_CR21","doi-asserted-by":"crossref","unstructured":"Hoare, C. A. R. (1975). Parallel programming: An axiomatic approach. Computer Languages, 1(2), 151\u2013160. Also have hard copy.","DOI":"10.1016\/0096-0551(75)90014-4"},{"key":"9621_CR22","volume-title":"Communicating sequential processes","author":"CAR Hoare","year":"1985","unstructured":"Hoare, C. A. R. (1985). Communicating sequential processes. Prentice Hall."},{"issue":"2","key":"9621_CR23","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/BF00264034","volume":"3","author":"CAR Hoare","year":"1974","unstructured":"Hoare, C. A. R., & Lauer, P. E. (1974). Consistent and complementary formal theories of the semantics of programming languages. Acta Informatica, 3(2), 135\u2013153. https:\/\/doi.org\/10.1007\/BF00264034","journal-title":"Acta Informatica"},{"key":"9621_CR24","unstructured":"Jackson, D. N. (2012). Software abstractions: Logic, language, and analysis. MIT."},{"key":"9621_CR25","unstructured":"Jones, C. B. (1980). Software development: A rigorous approach. Prentice Hall International. http:\/\/portal.acm.org\/citation.cfm?id=539771"},{"key":"9621_CR26","unstructured":"Jones, C. B. (1981). Development methods for computer programs including a notion of interference. PhD thesis, Oxford University. Printed as: Programming Research Group, Technical Monograph 25."},{"issue":"2","key":"9621_CR27","doi-asserted-by":"publisher","first-page":"26","DOI":"10.1109\/MAHC.2003.1203057","volume":"25","author":"CB Jones","year":"2003","unstructured":"Jones, C. B. (2003). The early search for tractable ways of reasoning about programs. IEEE Annals of the History of Computing, 25(2), 26\u201349.","journal-title":"IEEE Annals of the History of Computing"},{"key":"9621_CR28","doi-asserted-by":"crossref","unstructured":"Jones, C. B. (2017). Turing\u2019s 1949 paper in context. Lecture notes in computer scienceIn J. Kari, F. Manea, & I. Petre (Eds.), Computability in Europe 2017 (Vol. 10307, pp. 21\u201341). Springer.","DOI":"10.1007\/978-3-319-58741-7_4"},{"issue":"5","key":"9621_CR29","doi-asserted-by":"publisher","first-page":"972","DOI":"10.1016\/j.jlamp.2016.01.002","volume":"85","author":"CB Jones","year":"2016","unstructured":"Jones, C. B., & Hayes, I. J. (2016). Possible values: exploring a concept for concurrency. Journal of Logical and Algebraic Methods in Programming, 85(5), 972\u2013984. https:\/\/doi.org\/10.1016\/j.jlamp.2016.01.002","journal-title":"Journal of Logical and Algebraic Methods in Programming"},{"key":"9621_CR30","doi-asserted-by":"publisher","unstructured":"Jones, C. B., & Misra, J. (2021). Finding effective abstractions. In C. B. Jones & J. Misra (Eds.), Theories of programming: The life and works of Tony Hoare (pp. 23\u201340). ACM. https:\/\/doi.org\/10.1145\/3477355","DOI":"10.1145\/3477355"},{"key":"9621_CR31","unstructured":"King, J. C. (1969). A program verifier. PhD thesis, Department of Computer Science, Carnegie-Mellon University."},{"key":"9621_CR32","unstructured":"King, J. C. (1971). A program verifier. In C. V. Freiman, J. E. Griffith, & J. L. Rosenfeld (Eds.), Information processing, proceedings of IFIP congress 1971 (pp. 234\u2013249). North-Holland."},{"key":"9621_CR33","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1109\/TSE.1977.229904","volume":"3","author":"L Lamport","year":"1977","unstructured":"Lamport, L. (1977). Proving the correctness of mutiprocess programs. IEEE Transactions on Software Engineering, 3, 125\u2013143. https:\/\/doi.org\/10.1109\/TSE.1977.229904","journal-title":"IEEE Transactions on Software Engineering"},{"key":"9621_CR34","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1016\/0066-4138(69)90005-6","volume":"6","author":"P Lucas","year":"1969","unstructured":"Lucas, P., & Walk, K. (1969). On the formal description of pl\/i. Annual Review in Automatic Programming, 6, 105\u2013182.","journal-title":"Annual Review in Automatic Programming"},{"key":"9621_CR35","unstructured":"Manna, Z. (1968). Termination of algorithms. PhD thesis, Carnegie-Mellon University. https:\/\/apps.dtic.mil\/dtic\/tr\/fulltext\/u2\/670558.pdf"},{"key":"9621_CR36","unstructured":"Manna, Z. (1969a). The correctness of non-deterministic programs. Memo AI-95, Department of Computer Science, Stanford University."},{"key":"9621_CR37","doi-asserted-by":"publisher","unstructured":"Manna, Z. (1969b). The correctness of programs. Journal of Computer and System Sciences, 3(2), 119\u2013127. https:\/\/doi.org\/10.1016\/S0022-0000(69)80009-7","DOI":"10.1016\/S0022-0000(69)80009-7"},{"key":"9621_CR38","doi-asserted-by":"publisher","unstructured":"Manna, Z. (1969c). Properties of programs and the first-order predicate calculus. Journal of the ACM, 16(2), 244\u2013255. https:\/\/doi.org\/10.1145\/321510.321516","DOI":"10.1145\/321510.321516"},{"issue":"2","key":"9621_CR39","doi-asserted-by":"publisher","first-page":"139","DOI":"10.1109\/MAHC.1984.10017","volume":"6","author":"FL Morris","year":"1984","unstructured":"Morris, F. L., & Jones, C. B. (1984). An early program proof by alan turing. Annals of the History of Computing, 6(2), 139\u2013143. https:\/\/doi.org\/10.1109\/MAHC.1984.10017","journal-title":"Annals of the History of Computing"},{"issue":"5","key":"9621_CR40","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1145\/360051.360224","volume":"19","author":"S Owicki","year":"1976","unstructured":"Owicki, S., & Gries, D. (1976). Verifying properties of parallel programs: an axiomatic approach. Communications of the ACM, 19(5), 279\u2013285.","journal-title":"Communications of the ACM"},{"key":"9621_CR41","unstructured":"Owicki, S. S. (1975). Axiomatic proof techniques for parallel programs. PhD thesis, Department of Computer Science, Cornell University, published as technical report 75-251."},{"key":"9621_CR42","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1007\/BF00268134","volume":"6","author":"SS Owicki","year":"1976","unstructured":"Owicki, S. S., & Gries, D. (1976). An axiomatic proof technique for parallel programs i. Acta Informatica, 6, 319\u2013340.","journal-title":"Acta Informatica"},{"key":"9621_CR43","doi-asserted-by":"publisher","unstructured":"Priestley, M. (2020). Flow diagrams, assertions, and formal methods. In T. K. Astarte (Ed.), HFM 2019\u2014history of formal methods workshop, Porto, Portugal, 7\u201311 October 2019, Revised selected papers, Part II, No. 12233. Lecture notes in computer science (pp. 15\u201334). Springer. https:\/\/doi.org\/10.1007\/978-3-030-54997-8","DOI":"10.1007\/978-3-030-54997-8"},{"key":"9621_CR44","doi-asserted-by":"crossref","unstructured":"Reisig, W. (1985). Petri Nets: An introduction. Monographs in theoretical computer science (Vol. 4). Springer.","DOI":"10.1007\/978-3-642-69968-9"},{"key":"9621_CR45","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-33278-4","volume-title":"Understanding Petri Nets: Modeling techniques, analysis methods, case studies","author":"W Reisig","year":"2013","unstructured":"Reisig, W. (2013). Understanding Petri Nets: Modeling techniques, analysis methods, case studies. Springer."},{"key":"9621_CR46","unstructured":"Turing, A. M. (1949). Checking a large routine. Report of a conference on high speed automatic calculating machines (pp. 67\u201369). University Mathematical Laboratory."}],"updated-by":[{"DOI":"10.1007\/s11023-025-09746-9","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2025,10,21]],"date-time":"2025-10-21T00:00:00Z","timestamp":1761004800000}}],"container-title":["Minds and Machines"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11023-023-09621-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11023-023-09621-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11023-023-09621-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,22]],"date-time":"2025-10-22T05:34:01Z","timestamp":1761111241000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11023-023-09621-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,23]]},"references-count":46,"journal-issue":{"issue":"S1","published-online":{"date-parts":[[2024,2]]}},"alternative-id":["9621"],"URL":"https:\/\/doi.org\/10.1007\/s11023-023-09621-5","relation":{},"ISSN":["1572-8641"],"issn-type":[{"value":"1572-8641","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,1,23]]},"assertion":[{"value":"14 May 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 January 2023","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"23 January 2023","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"20 October 2025","order":5,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":6,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"The original online version of this article was revised: In the paragraph beginning \u2018Manna and Ashcroft concede that...\u2019 under section \u2018Ashcroft and Manna (Stanford 1969\/1970)\u2019 in this article, the formula\n                      \n                      should have read\n                      \n                      .","order":7,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"21 October 2025","order":8,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":9,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":10,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s11023-025-09746-9","URL":"https:\/\/doi.org\/10.1007\/s11023-025-09746-9","order":11,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}