Advertisement

Formal Aspects of Computing

, Volume 31, Issue 6, pp 751–807 | Cite as

Fifty years of Hoare’s logic

  • Krzysztof R. AptEmail author
  • Ernst-Rüdiger Olderog
Original Article
  • 10 Downloads

Abstract

We present a history of Hoare’s logic.

Notes

Acknowledgements

We would like to thank all three reviewers for exceptionally detailed and helpful referee reports that led us to improve and expand the presentation.

References

  1. [ABB+16]
    Ahrendt W, Beckert B, Bubel R, Hähnle R, Schmitt PH, Ulbrich M (eds) (2016) Deductive software verification—the KeY book—from theory to practice, volume 10001 of Lecture notes in computer science. SpringerGoogle Scholar
  2. [ABC87]
    Apt, K.R., Bougé, L., Clermont, P.: Two normal form theorems for CSP programs. Inf Process Lett 26, 165–171 (1987)MathSciNetzbMATHCrossRefGoogle Scholar
  3. [AdB77]
    Apt KR, de Bakker JW (1977) Semantics and proof theory of pascal procedures. In: Salomaa A, Steinby M (eds) Automata, languages and programming: proceedings of the fourth colloquium, volume 52 of Lecture notes in computer science. Springer, pp 30–44Google Scholar
  4. [AdB90a]
    America, P., de Boer, F.S.: Proving total correctness of recursive procedures. Inf Comput 84(2), 129–162 (1990)MathSciNetzbMATHCrossRefGoogle Scholar
  5. [AdB90b]
    America P, de Boer FS (1990) A proof system for process creation. In: Broy M (ed) Programming concepts and methods: proceedings of the IFIP working group 2.2, 2.3 working conference on programming concepts and methods. North-Holland, pp 303–332Google Scholar
  6. [AdB19]
    Apt KR, de Boer FS (2019) Reasoning about call-by-value: a missing result in the history of Hoare's logic, arXiv:1909.06215
  7. [ÁdBdRS05]
    Ábrahám, E., de Boer, F.S., de Roever, W.P., Steffen, M.: An assertion-based proof system for multithreaded java. Theor Comput Sci 331(2–3), 251–290 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  8. [AdBO90]
    Apt KR, de Boer FS, Olderog E-R (1990) Proving termination of parallel programs. In: Feijen WHJ, van Gasteren AJM, Gries D, MisraJ (eds) Beauty is our business, a birthday salute to Edsger W.Dijkstra. Springer, New York, pp 0–6Google Scholar
  9. [AdBO09]
    Apt, K.R., de Boer, F.S., Olderog, E.-R.: Verification of sequential and concurrent programs, 3rd edn. Springer, New York (2009)zbMATHCrossRefGoogle Scholar
  10. [AdBOdG12]
    Apt, K.R., de Boer, F.S., Olderog, E.-R., de Gouw, S.: Verification of object-oriented programs: a transformational approach. J Comput Syst Sci 78(3), 823–852 (2012)MathSciNetzbMATHCrossRefGoogle Scholar
  11. [AFdR80]
    Apt, K.R., Francez, N., de Roever, W.P.: A proof system for communicating sequential processes. ACM Trans Program Lang Syst 2(3), 359–385 (1980)zbMATHCrossRefGoogle Scholar
  12. [AFK88]
    Apt, K.R., Francez, N., Katz, S.: Appraising fairness in distributed languages. Distrib Comput 2(4), 226–241 (1988)zbMATHCrossRefGoogle Scholar
  13. [AFPdS11]
    Almeida JB, Frade MJ, Pinto JS, de Sousa SM (2011) Rigorous software development—an introduction to program verification. Undergraduate topics in computer science. SpringerGoogle Scholar
  14. [AMMO09]
    Arthan R, Martin U, Mathiesen EA, Oliva P (2009) A general framework for sound and complete Floyd-Hoare logics. ACM Trans Comput Log 11(1):7:1–7:31MathSciNetzbMATHCrossRefGoogle Scholar
  15. [AMO13]
    Arthan, R., Martin, U., Oliva, P.: A Hoare logic for linear systems. Formal Asp Comput 25(3), 345–363 (2013)MathSciNetzbMATHCrossRefGoogle Scholar
  16. [AO81]
    Apt KR, Olderog E-R (1981) Proof rules dealing with fairness. In: Logic of programs, volume 131 of Lecture notes in computer science. Springer, pp 1–8Google Scholar
  17. [AO83]
    Apt, K.R., Olderog, E.-R.: Proof rules and transformations dealing with fairness. Sci Comput Program 3, 65–100 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  18. [AO91]
    Apt, K.R., Olderog, E.-R.: Verification of sequential and concurrent programs. Springer, New York (1991)zbMATHCrossRefGoogle Scholar
  19. [AP86]
    Apt, K.R., Plotkin, G.D.: Countable nondeterminism and random assignment. J ACM 33(4), 724–767 (1986)Google Scholar
  20. [APS84]
    Apt, K.R., Pnueli, A., Stavi, J.: Fair termination revisited with delay. Theor Comput Sci 33, 65–84 (1984)MathSciNetzbMATHCrossRefGoogle Scholar
  21. [Apt81]
    Apt, K.R.: Ten years of Hoare's logic, a survey, part I. ACM Trans Program Lang Syst 3, 431–483 (1981)zbMATHCrossRefGoogle Scholar
  22. [Apt83]
    Apt, K.R.: Formal justification of a proof system for communicating sequential processes. J ACM 30, 197–216 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  23. [Apt84]
    Apt, K.R.: Ten years of Hoare's logic, a survey, part II: nondeterminism. Theor Comput Sci 28, 83–109 (1984)zbMATHCrossRefGoogle Scholar
  24. [Apt86]
    Apt, K.R.: Correctness proofs of distributed termination algorithms. ACM Trans Program Lang Syst 8, 388–405 (1986)zbMATHCrossRefGoogle Scholar
  25. [Bac80]
    Back R-JR (1980) Correctness preserving program refinements: proof theory and applications. Technical report 131, Mathematisch Centrum, AmsterdamGoogle Scholar
  26. [Bac86]
    Backhouse RC (1986) Program construction and verification. Prentice-Hall International, Englewood CliffsGoogle Scholar
  27. [Bal06]
    Balser M (2006) Verifying concurrent systems with symbolic execution—temporal reasoning is symbolic execution with a little induction. PhD thesis, University of Augsburg. Shaker VerlagGoogle Scholar
  28. [BCD+05]
    Barnett M, Chang BE, DeLine R, Jacobs B, Leino KRM (2005) Boogie: a modular reusable verifier for object-oriented programs. In: de Boer FS, Bonsangue MM, Graf S, de Roever WP (eds) Formal methods for components and objects, 4th international symposium, FMCO 2005, revised lectures, volume 4111 of Lecture notes in computer science. Springer, pp 364–387Google Scholar
  29. [Ben04]
    Benton N (2004) Simple relational correctness proofs for static analyses and program transformations. In: Jones ND, Leroy X (eds) Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on principles of programming languages (POPL 2004).ACM, pp 14–25Google Scholar
  30. [Ben12]
    Ben-Ari, M.: Mathematical logic for computer science, 3rd edn. Springer (2012)Google Scholar
  31. [BG87]
    Blass A, Gurevich Y (1987) Existential fixed-point logic. In: Börger E (ed) Computation theory and logic. Springer, pp 20–36Google Scholar
  32. [BGA+14]
    Barthe G, Gaboardi M, Arias EJG, Hsu J, Kunz C, Strub P (2014) Proving differential privacy in Hoare logic. In: IEEE 27th computer security foundations symposium (CSF 2014). IEEE Computer Society, pp411–424Google Scholar
  33. [BGB09]
    Barthe G, Grégoire B, Béguelin SZ (2009) Formal certification of code-based cryptographic proofs. In: Shao Z, PierceBC (eds) Proceedings of the 36th ACM SIGPLAN-SIGACT symposiumon principles of programming languages, POPL 2009. ACM, pp 90–101Google Scholar
  34. [BH16]
    Bubel R, Hähnle R (2016) KeY-Hoare. In: Deductive software verification—the KeY book—from theory to practice, volume 10001 of Lecture notes in computer science. Springer, pp 571–589Google Scholar
  35. [BKOB13]
    Barthe G, Köpf B, Olmedo F, Béguelin SZ (2013) Probabilistic relational reasoning for differential privacy. ACM Trans Program Lang Syst 35(3):9:1–9:49zbMATHCrossRefGoogle Scholar
  36. [BPS01]
    Bergstra JA, Ponse A, Smolka SA (eds) (2001) Handbook of process algebra. North-Holland/ElsevierGoogle Scholar
  37. [BR16]
    Baltag A, Renne B (2016) Dynamic epistemic logic. Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/archives/win2016/entries/dynamic-epistemic
  38. [Bro07]
    Brookes, S.: A semantics for concurrent separation logic. Theor Comput Sci 375(1–3), 227–270 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  39. [BRS+00]
    Balser, M., Reif, W., Schellhorn, G., Stenzel, K., Thums, A.: Formal system development in KIV. In: Maibaum, T. (ed.) Proceedings fundamental approaches to software engineering, volume 1783 of Lecture notes in computer science, pp. 363–366. Springer (2000)Google Scholar
  40. [BT82a]
    Bergstra, J.A., Tucker, J.V.: Some natural structures which fail to possess a sound and decidable Hoare-like logic for their while-programs. Theor Comput Sci 17, 303–315 (1982)MathSciNetzbMATHCrossRefGoogle Scholar
  41. [BT82b]
    Bergstra, J.A., Tucker, J.V.: Expressiveness and the completeness of Hoare's logic. J Comput Syst Sci 25(3), 267–284 (1982)MathSciNetzbMATHCrossRefGoogle Scholar
  42. [BvW08]
    Back, R.-J., von Wright, J.: Refinement calculus: a systematic introduction. Springer, New York (2008)zbMATHGoogle Scholar
  43. [CDE+16]
    Certezeanu, R., Drossopoulou, S., Egelund-Müller, B., Leino, K.R.M., Sivarajan, S., Wheel house, M.J.: Quicksort revisited–verifyingalternative versions of quicksort. In: Ábrahám, E., Bonsangue, M.M., Johnsen, E.B. (eds.) Theory and practice of formalmethods–essays dedicated to frank de boer on the occasion of his60th birthday. Lecture notes in computer science, vol. 9660, pp. 407–426. Springer (2016)Google Scholar
  44. [CGH83]
    Clarke, E.M., German, S.M., Halpern, J.Y.: Effective axiomatizations of Hoare logics. J ACM 30(3), 612–636 (1983)Google Scholar
  45. [CGH+93]
    Clarke EM, Grumberg O, Hiraishi H, Jha S, Long DE, McMillan KL, NessLA (1993) Verification of the futurebus+ cache coherence protocol. In: Agnew D, Claesen LJM, Camposano R (eds) Computer hardware description languages and their applications (CHDL '93), volume A-32 of IFIP transactions. North-Holland, pp 15–30Google Scholar
  46. [CGJ+03]
    Clarke, E., Grumberg, O., Jha, S., Lu, Y., Veith, H.: Counterexample-guided abstraction refinement for symbolic model checking. J ACM 50(5), 752–794 (2003)MathSciNetzbMATHCrossRefGoogle Scholar
  47. [CH72]
    Clint, M., Hoare, C.A.R.: Program proving: jumps and functions. Acta Inform 1, 214–224 (1972)zbMATHCrossRefGoogle Scholar
  48. [Chl13]
    Chlipala, A.: Certified programming with dependent types–a pragmatic introduction to the Coq Proof Assistant. MIT Press (2013)Google Scholar
  49. [CHVB18]
    Clarke EM, Henzinger TA, Veith H, Bloem R (eds)(2018) Handbook of model checking. SpringerGoogle Scholar
  50. [Cla76]
    Clarke EM (1976) Completeness and incompleteness theorems for Hoare-like axiom systems. PhD thesis, Computer Science Department, Cornell University USAGoogle Scholar
  51. [Cla79]
    Clarke, E.M.: Programming language constructs for which it is impossible to obtain good Hoare axiom systems. J ACM 26(1), 129–147 (1979)MathSciNetzbMATHCrossRefGoogle Scholar
  52. [Cla85]
    Clarke EM (1985) The characterization problem for Hoare logics. In: Hoare CAR, Shepherdson JC (eds) Mathematical logic and programming languages. Prentice-Hall International, Englewood Cliffs, pp 89–106Google Scholar
  53. [Cli73]
    Clint, M.: Program proving: coroutines. Acta Inform 2, 50–63 (1973)CrossRefGoogle Scholar
  54. [CO81]
    Cartwright, R., Oppen, D.C.: The logic of aliasing. Acta Inform 15, 365–384 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  55. [Coo78]
    Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM J Comput 7(1), 70–90 (1978)MathSciNetzbMATHCrossRefGoogle Scholar
  56. [Coo81]
    Cook, S.A.: Corrigendum: soundness and completeness of an axiom system for program verification. SIAM J Comput 10(3), 612 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  57. [Cou90]
    Cousot P (1990) Methods and logics for proving programs. In: Handbook of theoretical computer science, volume B: formal models and sematics (B). Elsevier, pp 841–994Google Scholar
  58. [CPR11]
    Cook, B., Podelski, A., Rybalchenko, A.: Proving program termination. Commun ACM 54(5), 88–98 (2011)CrossRefGoogle Scholar
  59. [dB75]
    de Bakker, J.W.: Inleiding Bewijsmethoden. Colloquium program mcorrectheid, MC Syllabus 21, pp. 3–17. MathematischCentrum, Amsterdam (1975)Google Scholar
  60. [dB80]
    de Bakker, J.W.: Mathematical theory of program correctness. Prentice-Hall International, Englewood Cliffs (1980)Google Scholar
  61. [dB91]
    de Boer FS (1991) A compositional proof system for dynamic process creation. In: LICS. IEEE Computer Society, pp 399–405Google Scholar
  62. [dB99]
    de Boer FS (1999) A WP-calculus for OO. In: FoSSaCS, volume 1578 of Lecture notes in computer science. Springer, pp 135–149Google Scholar
  63. [dBP03]
    de Boer FS, Pierik C (2003) How to cook a complete Hoare logic foryour pet OO language. In: FMCO, volume 3188 of Lecture notesin computer science. Springer, pp 111–133Google Scholar
  64. [DDH72]
    Dahl OJ, Dijkstra EW, Hoare CAR (eds) (1972). Structured programming. Academic Press LtdGoogle Scholar
  65. [DF88]
    Dijkstra EW, Feijen WHJ (1988) A method of programming. Addison-WesleyGoogle Scholar
  66. [dGdBB+19]
    de Gouw, S., de Boer, F.S., Bubel, R., Hähnle, R., Rot, J., Steinhöfel, D.: Verifying openjdk's sort method for generic collections. J Autom Reason 62(1), 93–126 (2019)MathSciNetzbMATHCrossRefGoogle Scholar
  67. [dGR16]
    de Gouw, S., Rot, J.: Effectively eliminating auxiliaries. In: Ábrahám, E., Bonsangue, M.M., Johnsen, E.B. (eds.) Theory and practice of formal methods–essays dedicated to frank de boer on the occasion of his 60th birthday. Lecture notes in computer science, vol. 9660, pp. 226–241. Springer (2016)Google Scholar
  68. [dHdV02]
    den Hartog, J., de Vink, E.P.: Verifying probabilistic programs using a Hoare like logic. Int J Found Comput Sci 13(3), 315–340 (2002)MathSciNetzbMATHCrossRefGoogle Scholar
  69. [Dij68]
    Dijkstra, E.W.: Cooperating sequential processes. Genuys F(ed) Programming languages: NATO advanced study institute, pp. 43–112. Academic Press, London (1968)CrossRefGoogle Scholar
  70. [Dij75]
    Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Commun ACM 18, 453–457 (1975)MathSciNetzbMATHCrossRefGoogle Scholar
  71. [Dij76a]
    Dijkstra, E.W.: A discipline of programming. Prentice-Hall, Englewood Cliffs (1976)zbMATHGoogle Scholar
  72. [Dij76b]
    Dijkstra EW (1976) A great improvement. http://www.cs.utexas.edu/users/EWD/ewd05xx/EWD573.PDF,published as [Dij82]
  73. [Dij82]
    Dijkstra EW (1982) A great improvement. In: Selected writings on computing: a personal perspective. Springer, , pp 217–219Google Scholar
  74. [DJ83]
    Damm, W., Josko, B.: A sound and relatively complete Hoare-logic for a language with higher type procedures. Acta Inform 20, 59–101 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  75. [dMB08]
    de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and algorithms for the construction and analysis of systems, TACAS 2008, volume 4963 of Lecture notes in computer science, pp. 337–340. Springer (2008)Google Scholar
  76. [dRdBH+01]
    de Roever WP, de Boer FS, Hannemann U, Hooman J, Lakhnech Y, Poel M, Zwiers J (2001) Concurrency verification: introduction to compositional and noncompositional methods, volume 54 of Cambridge tracts in theoretical computer science. Cambridge University PressGoogle Scholar
  77. [DS90]
    Dijkstra, E.W., Scholten, C.S.: Predicate calculus and program semantics. Springer, New York (1990)zbMATHCrossRefGoogle Scholar
  78. [EC82]
    Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci Comput Program 2(3), 241–266 (1982)zbMATHCrossRefGoogle Scholar
  79. [Eng17]
    Engelmann B (2017) Techniques for the verification of dynamically typed programs. PhD thesis, University of Oldenburg, GermanyGoogle Scholar
  80. [EO16]
    Engelmann, B., Olderog, E.-R.: A sound and complete Hoare logic for dynamically-typed, object-oriented programs. In: Ábrahám, E., Bonsangue, M.M., Johnsen, E.B. (eds.) Theory and practice of formal methods–essays dedicated to frank de boer on the occasion of his 60th birthday. Lecture notes in computer science, vol. 9660, pp. 173–193. Springer (2016)Google Scholar
  81. [FH71]
    Foley M, Hoare CAR (1971) Proof of a recursive program: quicksort. Comput J 14(4):391–395MathSciNetzbMATHCrossRefGoogle Scholar
  82. [Fil07]
    Filli├ótre, J.-C.: Formal proof of a program: find. Sci Comput Program 64(3), 332–340 (2007)MathSciNetCrossRefGoogle Scholar
  83. [Flo67]
    Floyd R (1967) Assigning meaning to programs. In: Schwartz JT (ed)Proceedings of symposium on applied mathematics 19, mathematical aspects of computer science. American Mathematical Society, New York, pp 19–32Google Scholar
  84. [FMV14]
    Furia CA, Meyer B, Velder S (2014) Loop invariants: analysis, classification, and examples. ACM Comput Surv46(3):34:1–34:51zbMATHCrossRefGoogle Scholar
  85. [Fra86]
    Francez, N.: Fairness. Springer, New York (1986)zbMATHCrossRefGoogle Scholar
  86. [Fra92]
    Francez N (1992) Program verification. Addison-Wesley, ReadingGoogle Scholar
  87. [GCH89]
    German, S.M., Clarke, E.M., Halpern, J.Y.: Reasoning about procedures as parameters in the language L4. Inf Comput 83(3), 265–359 (1989)zbMATHCrossRefGoogle Scholar
  88. [GFK84]
    Grumberg O, Francez N, Katz S (1984) Fair termination of communicating processes. In: Proceedings of the third annual ACM symposium on principles of distributed computing, Vancouver, B.C., Canada, August 27–29, 1984. ACM, pp 254–265Google Scholar
  89. [GFMdR81]
    Grumberg O, Francez N, Makowsky JA, de Roever WP (1981) A proof rule for fair termination of guarded commands. In: de Bakker J, van Vliet J (eds) Proceedings of the international symposium on algorithmic languages, pp 339–416Google Scholar
  90. [GFMdR85]
    Grumberg O, Francez N, Makowsky JA, de Roever WP (1985)A proof rule for fair termination of guarded commands. Inf Control 66(1/2):83–102MathSciNetzbMATHCrossRefGoogle Scholar
  91. [GL80]
    Gries, D., Levin, G.: Assignment and procedure call proof rules. ACM Trans Program Lang Syst 2(4), 564–579 (1980)zbMATHCrossRefGoogle Scholar
  92. [GMW79]
    Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. Lecture notes in computer science, vol. 78. Springer (1979)Google Scholar
  93. [Gor75]
    Gorelick GA (1975) A complete axiomatic system for proving assertions about recursive and nonrecursive programs. Technical report 75, Department of Computer Science, University of Toronto.https://archive.org/details/ACompleteAxiomaticSystemForProvingAssertionsAboutRecursiveAnd
  94. [Gor88]
    Gordon MJC (1988) Programming language theory and its implementation–applicative and imperative paradigms. Prentice Hall International series in Computer Science. Prentice HallGoogle Scholar
  95. [Gri78]
    Gries D (March 1978) The multiple assignment statement. IEEE Trans Softw Eng SE-4:89–93zbMATHCrossRefGoogle Scholar
  96. [Gri81]
    Gries, D.: The science of programming. Springer, New York (1981)zbMATHCrossRefGoogle Scholar
  97. [Har79]
    Harel D (1979) First-order dynamic logic. Lecture notes in computer science 68. Springer, New YorkGoogle Scholar
  98. [HdR86]
    Hooman J, de Roever WP (1986) The quest goes on: a survey of proofsystems for partial correctness of CSP. In: Current trends in concurrency. Lecture notes in computer science 224. Springer, New York, pp 343–395CrossRefGoogle Scholar
  99. [HJ00]
    Huisman M, Jacobs B (2000) Java program verification via a Hoarelogic with abrupt termination. In: Fundamental approaches to software engineering, third internationsl conference, FASE 2000, volume 1783 of Lecture notes in computer science. Springer, pp 284–303Google Scholar
  100. [HKT00]
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. MIT Press, Cambridge (2000)zbMATHCrossRefGoogle Scholar
  101. [HL74]
    Hoare, C.A.R., Lauer, P.E.: Consistent and complementary formal theories of the semantics of programming languages. Acta Inform 3, 135–153 (1974)MathSciNetzbMATHGoogle Scholar
  102. [HN18]
    Haslbeck MPL, Nipkow T (2018) Hoare logics for time bounds. Archive of formal proofs. http://isa-afp.org/entries/Hoare_Time.html. Formal proof developmentzbMATHCrossRefGoogle Scholar
  103. [Hoa61]
    Hoare, C.A.R.: Algorithm 64: quicksort. Commun ACM 4(7), 321 (1961)CrossRefGoogle Scholar
  104. [Hoa69]
    Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12:576–580, 583zbMATHCrossRefGoogle Scholar
  105. [Hoa71a]
    Hoare CAR (1971) Procedures and parameters: an axiomatic approach. In: Engeler E (ed) Proceedings of symposium on the semantics of algorithmic languages. Lecture notes in mathematics 188. Springer, New York, pp 102–116Google Scholar
  106. [Hoa71b]
    Hoare, C.A.R.: Proof of a program: FIND. Commun ACM 14(1), 39–45 (1971)zbMATHCrossRefGoogle Scholar
  107. [Hoa72a]
    Hoare CAR (1972) An axiomatic definition of the programming language PASCAL. In: International sympoisum on theoretical programming, volume 5 of Lecture notes in computer science. Springer, pp 1–16Google Scholar
  108. [Hoa72b]
    Hoare, C.A.R.: Proof of a structured program: 'the sieve of Eratosthenes'. Comput J 15(4), 321–325 (1972)MathSciNetzbMATHCrossRefGoogle Scholar
  109. [Hoa72c]
    Hoare, C.A.R.: Towards a theory of parallel programming. In: Perrot, R.H. (ed.) HoareCAR, pp. 61–71. Operating systems techniques. Academic Press, London (1972)CrossRefGoogle Scholar
  110. [Hoa75]
    Hoare, C.A.R.: Parallel programming: an axiomatic approach. Comput Lang 1(2), 151–160 (1975)Google Scholar
  111. [Hoa78]
    Hoare, C.A.R.: Communicating sequential processes. Commun ACM 21, 666–677 (1978)Google Scholar
  112. [HOP10]
    Hoenicke, J., Olderog, E.-R., Podelski, A.: Fairness for dynamic control. In: Esparza, J., Majumdar, R. (eds.) Tools and algorithms for the construction and analysis of systems, 16th international conference, (TACAS 2010). Lecture notes in computer science, vol. 6015, pp. 251–265. Springer (2010)Google Scholar
  113. [HP15]
    Hoenicke, J., Podelski, A.: Fairness for infinitary control. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct system design–symposium in Honor of Ernst-Rüdiger olderog on the occasion of his 60th birthday. Lecture notes in computer science, vol. 9360, pp. 33–43. Springer (2015)Google Scholar
  114. [HW73]
    Hoare, C.A.R., Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Inform 2, 335–355 (1973)zbMATHCrossRefGoogle Scholar
  115. [INM84]
    Limited, I.N.M.O.S.: Occam programming manual. Prentice-Hall International, Englewood Cliffs (1984)Google Scholar
  116. [Jon81]
    Jones CB (1981) Developing methods for computer programs including a notion of interference. PhD thesis, University of Oxford, UKGoogle Scholar
  117. [Jon83]
    Jones, C.B.: Tentative steps toward a development method for interfering programs. ACM Trans Program Lang Syst 5(4), 596–619 (1983)zbMATHCrossRefGoogle Scholar
  118. [Jon03]
    Jones, C.B.: The early search for tractable ways of reasoning about programs. IEEE Ann Hist Comput 25(2), 26–49 (2003)MathSciNetCrossRefGoogle Scholar
  119. [JP04]
    Jacobs B, Poll E (2004) Java program verification at nijmegen: developments and perspective. In: Futatsugi K, Mizoguchi F, YonezakiN (eds) Software security—heories and systems, second Mext-NSF-JSPS international symposium, ISSS 2003, Tokyo, Japan, November 4–6, 2003, revised papers, volume 3233 of Lecture notes in computer science. Springer, pp 134–153Google Scholar
  120. [JR10]
    Jones CB, Roscoe AW (2010) Insight, inspiration and collaboration. In: Roscoe AW, Jones CB, Wood KR (eds) Reflections on the work of C.A.R. Hoare. Springer, pp 1–32Google Scholar
  121. [JW75]
    Jensen, K., Wirth, N.: PASCAL user manual and report. Springer (1975)Google Scholar
  122. [Kal90]
    Kaldewaij, A.: Programming: the derivation of algorithms. Prentice-Hall International, Englewood Cliffs (1990)Google Scholar
  123. [KGJ+15]
    Katoen, J., Gretz, F., Jansen, N., Kaminski, B.L., Olmedo, F.: Understanding probabilistic programs. In: Meyer, R., Platzer, A., Wehrheim, H. (eds.) Correct system design–symposium in Honor of Ernst-Rüdiger olderog on the occasion of his 60th birthday, volume 9360 of Lecture notes in computer science, pp. 15–32. Springer (2015)Google Scholar
  124. [Kin69]
    King J (1969) Developing methods for computer programs including a notion of interference. PhD thesis, Department of Computer Science, Carnegie-Mellon University, Pittsburgh USAGoogle Scholar
  125. [Kle98]
    Kleymann T (1998) Hoare logic and VDM : machine-checked soundness and completeness proofs. PhD thesis, University of Edinburgh UKGoogle Scholar
  126. [Kle99]
    Kleymann, T.: Hoare logic and auxiliary variables. Formal Asp Comput 11(5), 541–566 (1999)zbMATHCrossRefGoogle Scholar
  127. [Koz00]
    Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Trans Comput Log 1(1), 60–76 (2000)MathSciNetzbMATHCrossRefGoogle Scholar
  128. [KT01]
    Kozen, D., Tiuryn, J.: On the completeness of propositional Hoare logic. Inf Sci 139(3–4), 187–195 (2001)MathSciNetzbMATHCrossRefGoogle Scholar
  129. [Lam77]
    Lamport L (1977) Proving the correctness of multiprocess programs. IEEE Trans Softw Eng SE-3:2:125–143MathSciNetzbMATHCrossRefGoogle Scholar
  130. [Lam94]
    Lamport, L.: The temporal logic of actions. ACM Trans Program Lang Syst 16(3), 872–923 (1994)CrossRefGoogle Scholar
  131. [Lam02]
    Lamport, L.: Specifying systems, the TLA+ language and tools for hardware and software engineers. Addison-Wesley (2002)Google Scholar
  132. [Lan79]
    Langmaack H (1979) A proof of a theorem of Lipton on Hoare logic and applications. Technical report, Ber. 8003,Inst Inf Prakt Math, University of Kiel, GermanyGoogle Scholar
  133. [Lan82]
    Langmaack, H.: On the termination problem for finitely interpreted ALGOL-like programs. Acta Inform 18, 79–108 (1982)MathSciNetzbMATHCrossRefGoogle Scholar
  134. [Lau71]
    Lauer PE (1971) Consistent formal theories of the semantics of programming languages. Technical report 25. 121, IBM Laboratory ViennaGoogle Scholar
  135. [LCC+05]
    Leavens, G.T., Cheon, Y., Clifton, C., Ruby, C., Cok, D.R.: How the design of JML accommodates both runtime assertion checking and formal verification. Sci Comput Program 55(1–3), 185–208 (2005)MathSciNetzbMATHCrossRefGoogle Scholar
  136. [Lei10]
    Leino KRM (2010) Dafny: an automatic program verifier for functional correctness. In: Clarke EM, Voronkov A (eds) Logic for programming, artificial intelligence, and reasoning, LPAR-16, volume 6355 of Lecture notes in computer science. Springer, pp 348–370Google Scholar
  137. [LG81]
    Levin, G., Gries, D.: A proof technique for communicating sequential processes. Acta Inform 15, 281–302 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  138. [LGH+78]
    London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.J.: Proof rules for the programming language Euclid. Acta Inform 10, 1–26 (1978)zbMATHCrossRefGoogle Scholar
  139. [Lip75]
    Lipton, R.J.: Reduction: a method of proving properties of parallel programs. Commun ACM 18, 717–721 (1975)MathSciNetzbMATHCrossRefGoogle Scholar
  140. [Lip77]
    Lipton RJ (1977) A necessary and sufficient condition for the existence of Hoare logics. In: 18th annual symposium on foundations of computer science. IEEE Computer Society, pp 1–6Google Scholar
  141. [LO80]
    Langmaack, H., Olderog, E.-R.: Present-day Hoare-like systems for programming languages with procedures: power, limits and most likely expressions. In: de Bakker, J.W., van Leeuwen, J. (eds.) Automata, languages and programming, 7th colloquium, volume 85 of Lecture notes in computer science, pp. 363–373. Springer (1980)Google Scholar
  142. [LPS81]
    Lehmann DJ, Pnueli A, Stavi J (1981) Impartiality, justice, and fairness: the ethics of concurrent termination. In: Kariv O, Even S(eds) Proceedings of international colloquium on automata languages and programming (ICALP '81). Lecture notes in computer science 115. Springer, New York, pp 264–277zbMATHCrossRefGoogle Scholar
  143. [LS87]
    Loeckx, J., Sieber, K.: The foundation of program verification, 2nd edn. Teubner-Wiley, Stuttgart (1987)zbMATHCrossRefGoogle Scholar
  144. [Man74]
    Manna Z (1974) Mathematical theory of computation. Mc Graw-HillGoogle Scholar
  145. [Mey97]
    Meyer B (1997) Object-oriented software construction, 2nd edn. Prentice HallGoogle Scholar
  146. [Mil80]
    Milner R (1980) A calculus of communicating systems. Lecture notes in computer science 92, Springer, New YorkGoogle Scholar
  147. [Mil89]
    Milner, R.: Communication and concurrency. Prentice-Hall International, Englewood Cliffs (1989)zbMATHGoogle Scholar
  148. [MJ84]
    Morris, F.L., Jones, C.B.: An early program proof by Alan Turing. Ann Hist Comput 6, 139–143 (1984)MathSciNetzbMATHCrossRefGoogle Scholar
  149. [MM05]
    McIver A, Morgan C (2005) Abstraction, refinement and proof for probabilistic systems. Monographs in computer science. SpringerGoogle Scholar
  150. [Moi83]
    Moitra, A.: On Apt, Francez, and de Roever's "A proof system for communicating sequential processes". ACM Trans Program Lang Syst 5(3), 500–501 (1983)MathSciNetCrossRefGoogle Scholar
  151. [Mor94]
    Morgan C (1994) Programming from specifications, 2nd end. Prentice-Hall International, LondonGoogle Scholar
  152. [MP74]
    Manna, Z., Pnueli, A.: Axiomatic approach to total correctness of programs. Acta Inform 3, 253–263 (1974)MathSciNetzbMATHCrossRefGoogle Scholar
  153. [MP91]
    Manna, Z., Pnueli, A.: The temporal logic of reactive and concurrent systems–specification. Springer, New York (1991)zbMATHGoogle Scholar
  154. [MP95]
    Manna, Z., Pnueli, A.: Temporal verification of reactive systems–safety. Springer, New York (1995)zbMATHCrossRefGoogle Scholar
  155. [MS87]
    Mirkowska, C., Salwicki, A.: Algorithmic logic. Kluwer Academic Publishers, Norwell (1987)zbMATHGoogle Scholar
  156. [Nau66]
    Naur, P.: Proof of algorithms by general snapshots. BIT Numer Math 6(4), 310–316 (1966)CrossRefGoogle Scholar
  157. [NBB+63]
    Naur P, Backus J, Bauer F, Green J, Katz C, McCarthy J, Perlis A, Rutishauser H, Samelson K, Vauquois B, Wegstein J, van WijngaardenA, Woodger M (1963) Report on the algorithmic language ALGOL 60. Numer Math 4:420–453Google Scholar
  158. [NCMM09]
    Nordio M, Calcagno C, Müller P, Meyer B (2009) A sound and complete program logic for eiffel. In: Oriol M, Meyer B (eds) Objects, components, models and patterns, 47th international conference, TOOLS EUROPE 2009, Zurich, Switzerland, June 29–July3, 2009. Proceedings, volume 33 of Lecture notes in business information processing. Springer, pp 195–214CrossRefGoogle Scholar
  159. [Nie87]
    Nielson, H.R.: A Hoare-like proof system for analysing the computation time of programs. Sci Comput Program 9(2), 107–136 (1987)MathSciNetzbMATHCrossRefGoogle Scholar
  160. [Nip02a]
    Nipkow T (2002) Hoare logics in Isabelle/HOL. In: SchwichtenbergH, Steinbrüggen R (eds) Proof and system-reliability, volume 62 of NATO science series. Springer, pp 341–367Google Scholar
  161. [Nip02b]
    Nipkow T (2002) Hoare logics for recursive procedures and unbounded nondeterminism. In: Proceedings of the computer science logic, 16th international workshop, CSL 2002, volume 2471 of Lecture notes in computer science. Springer, pp 103–119Google Scholar
  162. [NN99]
    Nipkow, T., Nieto, L.P.: Owicki/Gries in Isabelle/HOL. In: Finance, J.P. (ed.) Fundamental approaches in software enginering (FASE). Lecture notes in computer science, vol. 1577, pp. 188–203. Springer (1999)Google Scholar
  163. [NPW02]
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL–A proof assistant for higher-order logic. Lecture notes in computer science, vol. 2283. Springer (2002)Google Scholar
  164. [OA88]
    Olderog, E.-R., Apt, K.R.: Fairness in parallel programs, the transformational approach. ACM Trans Program Lang Syst 10, 420–455 (1988)CrossRefGoogle Scholar
  165. [OG76a]
    Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Inform 6, 319–340 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  166. [OG76b]
    Owicki, S., Gries, D.: Verifying properties of parallel programs: an axiomatic approach. Commun ACM 19, 279–285 (1976)MathSciNetzbMATHCrossRefGoogle Scholar
  167. [O'H07]
    O'Hearn, P.W.: Resources, concurrency, and local reasoning. Theor Comput Sci 375(1–3), 271–307 (2007)MathSciNetzbMATHCrossRefGoogle Scholar
  168. [O'H19]
    O'Hearn, P.W.: Separation logic. Commun ACM 62(2), 86–95 (2019)CrossRefGoogle Scholar
  169. [Old81]
    Olderog, E.-R.: Sound and complete Hoare-like calculi based on copy rules. Acta Inform 16, 161–197 (1981)MathSciNetzbMATHCrossRefGoogle Scholar
  170. [Old83a]
    Olderog E-R (1983) A characterization of Hoare's logic for programs with Pascal-like procedures. In: Proceedings of the 15th ACM symposium on theory of computing (STOC). ACM, pp 320–329Google Scholar
  171. [Old83b]
    Olderog, E.-R.: On the notion of expressiveness and the rule of adaptation. Theor Comput Sci 30, 337–347 (1983)MathSciNetzbMATHCrossRefGoogle Scholar
  172. [Old84]
    Olderog, E.-R.: Correctness of programs with Pascal-like procedures without global variables. Theor Comput Sci 30, 49–90 (1984)MathSciNetzbMATHCrossRefGoogle Scholar
  173. [OP10]
    Olderog, E.-R., Podelski, A.: Explicit fair scheduling for dynamic control. In: Dams, D., Hannemann, U., Steffen, M. (eds.) Concurrency, compositionality, and correctness, essays in Honor of Willem-Paul deRoever. Lecture notes in computer science, vol. 5930, pp. 96–117. Springer (2010)Google Scholar
  174. [ORS92]
    Owre, S., Rushby, J.M., Shankar, N.: PVS: A prototype verification system. In: Kapur, D. (ed.) Automated deduction(CADE-11), 11th international conference on automated deduction 1992, proceedings. Lecture notes in computer science, vol. 607, pp. 748–752. Springer (1992)Google Scholar
  175. [ORY01]
    O'Hearn, P.W., Reynolds, J.C., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) Computer science logic, 15th international workshop (CSL 2001), volume 2142 of Lecture notes in computer science, pp. 1–19. Springer (2001)Google Scholar
  176. [OW12]
    Olderog, E.-R., Wilhelm, R.: Turing und die Verifikation. Informatik Spektrum 35(4), 271–279 (2012)CrossRefGoogle Scholar
  177. [Owi75]
    Owicki S (1975) Axiomatic proof techniques for parallel programs. Outstanding dissertations in the computer sciences. Garland Publishing, New YorkGoogle Scholar
  178. [Owi76]
    Owicki S (1976) A consistent and complete deductive system for theverification of parallel programs. In: STOC. ACM, pp 73–86Google Scholar
  179. [Owi78]
    Owicki S (1978) Verifying concurrent programs with shared dataclasses. In: Neuhold EJ (ed) Proceedings of the IFIP working conference on formal description of programming concepts. North-Holland, Amsterdam, pp279–298Google Scholar
  180. [OYR04]
    O'Hearn PW, Yang H, Reynolds JC (2004) Separation and information hiding.In: Jones ND, Leroy X (eds) Proceedings of 31st symposium on principles of programming languages (POPL 2004). ACM, pp 268–280Google Scholar
  181. [PdB03]
    Pierik C, de Boer FS (2003) A syntax-directed Hoare logic for object-oriented programming concepts. In: FMOODS, volume 2884 of Lecture notes in computer science. Springer, pp 64–78Google Scholar
  182. [Pla08]
    Platzer, A.: Differential dynamic logic for hybrid systems. J Autom Reasoning 41(2), 143–189 (2008)MathSciNetzbMATHCrossRefGoogle Scholar
  183. [Pnu77]
    Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science, pp46–57Google Scholar
  184. [PR18]
    Piskac R, Rümmer P (eds) (2018) Verified software. Theories, tools, and experiments—10th international conference, VSTTE2018, Oxford, UK, July 18–19, 2018, Revised selected papers, volume 11294 of Lecture notes in computer science. SpringerzbMATHGoogle Scholar
  185. [Pra76]
    Pratt VR (1976) Semantical considerations on Floyd-Hoare logic. In: 17th annual symposium on foundations of computer science(FoCS 1976). IEEE Computer Society, pp 109–121Google Scholar
  186. [QS81]
    Queille JP, Sifakis J (1981) Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th international symposium on programming, ParisGoogle Scholar
  187. [Rey02]
    Reynolds JC (2002) Separation logic: a logic for shared mutable data structures. In: 17th IEEE symposium on logic in computer science (LICS 2002). IEEE Computer Society, pp 55–74Google Scholar
  188. [Sal70]
    Salwicki, A.: Formalized algorithmic languages. Bull Acad Pol Sci 18, 227–232 (1970)MathSciNetGoogle Scholar
  189. [Sch77]
    Schwarz, J.: Generic commands–a tool for partial correctness formalisms. Comput J 20, 151–155 (1977)MathSciNetzbMATHCrossRefGoogle Scholar
  190. [Sok77]
    Sokołowski S (1977) Total correctness for procedures. In: 6th symposium on mathematical foundations of computer science, volume 53 of Lecture notes in computer science. Springer, pp 475–483Google Scholar
  191. [Sok87]
    Sokołowski, S.: Soundness of Hoare's logic: an automated proof using LCF. ACM Trans Program Lang Syst 9(1), 100–120 (1987)CrossRefGoogle Scholar
  192. [Spi92]
    Spivey JM (1992) The Z notation: a reference manual, 2nd edn. Prentice HallGoogle Scholar
  193. [SS14]
    Sznuk T, Schubert A (2014) Tool support for teaching Hoare logic. In: Giannakopoulou D, Salaün G (eds) Software engineeringand formal methods—12th international conference (SEFM 2014), volume 8702 of Lecture notes in computer science. Springer, pp 332–346Google Scholar
  194. [Tar36]
    Tarski, A.: Der Wahrheitsbegriff in den formalisierten Sprachen. Studia Philosophica 1(3), 261–405 (1936)zbMATHGoogle Scholar
  195. [Tur49]
    Turing AM (1949) On checking a large routine. Report of a conference on high speed automatic calculating machines, pp67–69, 1949. University Mathematics Laboratory, Cambridge. (See also: F. L.Morris and Jones CB, An early program proof by Alan Turing,Annals of the History of Computing 6 pp 139–143, 1984)Google Scholar
  196. [TZ88]
    Tucker, J.V., Zucker, J.I.: Program correctness over abstract datatypes, with error-state semantics. North-Holland and CWI Monographs, Amsterdam (1988)zbMATHGoogle Scholar
  197. [Unr19]
    Unruh D (2019) Quantum relational Hoare logic. Proc ACM Program Lang 3(POPL):33:1–33:31CrossRefGoogle Scholar
  198. [vO99]
    von Oheimb D (1999) Hoare logic for mutual recursion and local variables.In: Foundations of software technology and theoretical computerscience, 19th conference, Chennai, India, December 13–15, 1999, proceedings, volume 1738 of Lecture notes in computer science. Springer,pp 168–180Google Scholar
  199. [vON02]
    von Oheimb D, Nipkow T (2002) Hoare logic for nanojava: auxiliary variables, side effects, and virtual methods revisited. In:Eriksson L, Lindsay PA (eds) FME 2002: formal methods—getting IT right, international symposium of formal methodsEurope, Copenhagen, Denmark, July 22–24, 2002, proceedings, volume2391 of Lecture notes in computer science. Springer, pp 89–105Google Scholar
  200. [vWMP+75]
    van Wijngaarden, A., Mailloux, B.J., Peck, J.E.L., Koster, C.H.A., Sintzoff, M., Lindsey, C.H., Meertens, L.G.L.T., Fisker, R.G.: Revised report on the algorithmic language ALGOL 68. Acta Inform 5, 1–236 (1975)zbMATHCrossRefGoogle Scholar
  201. [Wan78]
    Wand, M.: A new incompleteness result for Hoare's system. JACM 25(1), 168–175 (1978)MathSciNetzbMATHCrossRefGoogle Scholar
  202. [WH66]
    Wirth, N., Hoare, C.A.R.: A contribution to the development of ALGOL. Commun ACM 9(6), 413–432 (1966)zbMATHCrossRefGoogle Scholar
  203. [Win93]
    Winskel, G.: The formal semantics of programming languages–an introduction. MIT Press, Foundation of computing series (1993)zbMATHGoogle Scholar
  204. [Yin11]
    Ying M (2011) Floyd–Hoare logic for quantum programs. ACM Trans Program Lang Syst 33(6):19:1–19:49CrossRefGoogle Scholar
  205. [Yin19]
    Ying, M.: Toward automatic verification of quantum programs. Formal Asp Comput 31(1), 3–25 (2019)MathSciNetzbMATHCrossRefGoogle Scholar
  206. [Zöb88]
    Zöbel, D.: Normalform-Transformationen für CSP-Programme. Informatik: Forschung und Entwicklung 3, 64–76 (1988)Google Scholar

Copyright information

© British Computer Society 2019

Authors and Affiliations

  1. 1.CWIAmsterdamThe Netherlands
  2. 2.MIMUWUniversity of WarsawWarsawPoland
  3. 3.University of OldenburgOldenburgGermany

Personalised recommendations