×

zbMATH — the first resource for mathematics

Fifty years of Hoare’s logic. (English) Zbl 1427.68008
Summary: We present a history of Hoare’s logic.
MSC:
68-03 History of computer science
03B70 Logic in computer science
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] 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. Springer
[2] Apt, Kr; Bougé, L.; Clermont, P., Two normal form theorems for CSP programs, Inf Process Lett, 26, 165-171 (1987) · Zbl 0631.68026
[3] 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-44
[4] America, P.; De Boer, Fs, Proving total correctness of recursive procedures, Inf Comput, 84, 2, 129-162 (1990) · Zbl 0699.68024
[5] 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-332
[6] 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] Ábrahám, E.; De Boer, Fs; De Roever, Wp; Steffen, M., An assertion-based proof system for multithreaded java, Theor Comput Sci, 331, 2-3, 251-290 (2005) · Zbl 1070.68016
[8] Apt, Krzysztof R.; Boer, Frank S.; Olderog, Ernst-Rüdiger, Proving Termination of Parallel Programs, Beauty Is Our Business, 1-6 (1990), New York, NY: Springer New York, New York, NY · Zbl 1241.68047
[9] Apt, Kr; De Boer, Fs; Olderog, E-R, Verification of sequential and concurrent programs (2009), New York: Springer, New York · Zbl 1183.68361
[10] Apt, Kr; De Boer, Fs; Olderog, E-R; De Gouw, S., Verification of object-oriented programs: a transformational approach, J Comput Syst Sci, 78, 3, 823-852 (2012) · Zbl 1245.68062
[11] Apt, Kr; Francez, N.; De Roever, Wp, A proof system for communicating sequential processes, ACM Trans Program Lang Syst, 2, 3, 359-385 (1980) · Zbl 0468.68023
[12] Apt, Kr; Francez, N.; Katz, S., Appraising fairness in distributed languages, Distrib Comput, 2, 4, 226-241 (1988) · Zbl 0659.68023
[13] Almeida JB, Frade MJ, Pinto JS, de Sousa SM (2011) Rigorous software development—an introduction to program verification. Undergraduate topics in computer science. Springer
[14] Arthan, Rob; Martin, Ursula; Mathiesen, Erik A.; Oliva, Paulo, A general framework for sound and complete Floyd-Hoare logics, ACM Transactions on Computational Logic, 11, 1, 1-31 (2009) · Zbl 1351.03020
[15] Arthan, R.; Martin, U.; Oliva, P., A Hoare logic for linear systems, Formal Asp Comput, 25, 3, 345-363 (2013) · Zbl 1298.68163
[16] 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-8
[17] Apt, Kr; Olderog, E-R, Proof rules and transformations dealing with fairness, Sci Comput Program, 3, 65-100 (1983) · Zbl 0512.68014
[18] Apt, Kr; Olderog, E-R, Verification of sequential and concurrent programs (1991), New York: Springer, New York · Zbl 0733.68053
[19] Apt, Kr; Plotkin, Gd, Countable nondeterminism and random assignment. J ACM, 33, 4, 724-767 (1986) · Zbl 0627.68015
[20] Apt, Kr; Pnueli, A.; Stavi, J., Fair termination revisited with delay, Theor Comput Sci, 33, 65-84 (1984) · Zbl 0542.68015
[21] Apt, Kr, Ten years of Hoare’s logic, a survey, part I, ACM Trans Program Lang Syst, 3, 431-483 (1981) · Zbl 0471.68006
[22] Apt, Kr, Formal justification of a proof system for communicating sequential processes, J ACM, 30, 197-216 (1983) · Zbl 0503.68021
[23] Apt, Kr, Ten years of Hoare’s logic, a survey, part II: nondeterminism, Theor Comput Sci, 28, 83-109 (1984) · Zbl 0523.68015
[24] Apt, Kr, Correctness proofs of distributed termination algorithms, ACM Trans Program Lang Syst, 8, 388-405 (1986) · Zbl 0599.68017
[25] Back R-JR (1980) Correctness preserving program refinements: proof theory and applications. Technical report 131, Mathematisch Centrum, Amsterdam · Zbl 0451.68018
[26] Backhouse RC (1986) Program construction and verification. Prentice-Hall International, Englewood Cliffs
[27] Balser M (2006) Verifying concurrent systems with symbolic execution—temporal reasoning is symbolic execution with a little induction. PhD thesis, University of Augsburg. Shaker Verlag · Zbl 1100.68063
[28] 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-387
[29] 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-25 · Zbl 1325.68057
[30] Ben-Ari, M.: Mathematical logic for computer science, 3rd edn. Springer (2012) · Zbl 1248.03001
[31] Blass A, Gurevich Y (1987) Existential fixed-point logic. In: Börger E (ed) Computation theory and logic. Springer, pp 20-36
[32] 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-424
[33] 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-101
[34] 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-589
[35] Barthe, Gilles; Köpf, Boris; Olmedo, Federico; Zanella-Béguelin, Santiago, Probabilistic Relational Reasoning for Differential Privacy, ACM Transactions on Programming Languages and Systems, 35, 3, 1-49 (2013) · Zbl 1321.68182
[36] Bergstra JA, Ponse A, Smolka SA (eds) (2001) Handbook of process algebra. North-Holland/Elsevier · Zbl 0971.00006
[37] Baltag A, Renne B (2016) Dynamic epistemic logic. Stanford Encyclopedia of Philosophy. https://plato.stanford.edu/archives/win2016/entries/dynamic-epistemic
[38] Brookes, S., A semantics for concurrent separation logic, Theor Comput Sci, 375, 1-3, 227-270 (2007) · Zbl 1111.68021
[39] 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)
[40] Bergstra, Ja; Tucker, Jv, 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) · Zbl 0483.68033
[41] Bergstra, Ja; Tucker, Jv, Expressiveness and the completeness of Hoare’s logic, J Comput Syst Sci, 25, 3, 267-284 (1982) · Zbl 0549.68021
[42] Back, R-J; Von Wright, J., Refinement calculus: a systematic introduction (2008), New York: Springer, New York
[43] 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)
[44] Clarke, Em; German, Sm; Halpern, Jy, Effective axiomatizations of Hoare logics. J ACM, 30, 3, 612-636 (1983) · Zbl 0627.68010
[45] 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-30
[46] 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) · Zbl 1325.68145
[47] Clint, M.; Hoare, Car, Program proving: jumps and functions, Acta Inform, 1, 214-224 (1972) · Zbl 0229.68003
[48] Chlipala, A.: Certified programming with dependent types-a pragmatic introduction to the Coq Proof Assistant. MIT Press (2013) · Zbl 1288.68001
[49] Clarke EM, Henzinger TA, Veith H, Bloem R (eds)(2018) Handbook of model checking. Springer · Zbl 1390.68001
[50] Clarke EM (1976) Completeness and incompleteness theorems for Hoare-like axiom systems. PhD thesis, Computer Science Department, Cornell University USA
[51] Clarke, Em, Programming language constructs for which it is impossible to obtain good Hoare axiom systems, J ACM, 26, 1, 129-147 (1979) · Zbl 0388.68008
[52] 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-106
[53] Clint, M., Program proving: coroutines, Acta Inform, 2, 50-63 (1973)
[54] Cartwright, R.; Oppen, Dc, The logic of aliasing, Acta Inform, 15, 365-384 (1981) · Zbl 0445.68022
[55] Cook, Sa, Soundness and completeness of an axiom system for program verification, SIAM J Comput, 7, 1, 70-90 (1978) · Zbl 0374.68009
[56] Cook, Sa, Corrigendum: soundness and completeness of an axiomsystem for program verification, SIAM J Comput, 10, 3, 612 (1981) · Zbl 0466.68015
[57] 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-994
[58] Cook, B.; Podelski, A.; Rybalchenko, A., Proving program termination, Commun ACM, 54, 5, 88-98 (2011)
[59] de Bakker, J.W.: Inleiding Bewijsmethoden. Colloquium program mcorrectheid, MC Syllabus 21, pp. 3-17. MathematischCentrum, Amsterdam (1975)
[60] de Bakker, J.W.: Mathematical theory of program correctness. Prentice-Hall International, Englewood Cliffs (1980) · Zbl 0452.68011
[61] de Boer FS (1991) A compositional proof system for dynamic process creation. In: LICS. IEEE Computer Society, pp 399-405
[62] de Boer FS (1999) A WP-calculus for OO. In: FoSSaCS, volume 1578 of Lecture notes in computer science. Springer, pp 135-149
[63] 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-133 · Zbl 1104.68428
[64] Dahl OJ, Dijkstra EW, Hoare CAR (eds) (1972). Structured programming. Academic Press Ltd
[65] Dijkstra EW, Feijen WHJ (1988) A method of programming. Addison-Wesley
[66] De Gouw, S.; De Boer, Fs; 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) · Zbl 1468.68125
[67] 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)
[68] Den Hartog, J.; De Vink, Ep, Verifying probabilistic programs using a Hoare like logic, Int J Found Comput Sci, 13, 3, 315-340 (2002) · Zbl 1066.68081
[69] Dijkstra, Edsger W., Cooperating Sequential Processes, The Origin of Concurrent Programming, 65-138 (1968), New York, NY: Springer New York, New York, NY
[70] Dijkstra, Ew, Guarded commands, nondeterminacy and formal derivation of programs, Commun ACM, 18, 453-457 (1975) · Zbl 0308.68017
[71] Dijkstra, Ew, A discipline of programming (1976), Englewood Cliffs: Prentice-Hall, Englewood Cliffs
[72] Dijkstra EW (1976) A great improvement. http://www.cs.utexas.edu/users/EWD/ewd05xx/EWD573.PDF,published as [Dij82]
[73] Dijkstra EW (1982) A great improvement. In: Selected writings on computing: a personal perspective. Springer, , pp 217-219
[74] Damm, W.; Josko, B., A sound and relatively complete Hoare-logic for a language with higher type procedures, Acta Inform, 20, 59-101 (1983) · Zbl 0501.68008
[75] 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)
[76] 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 Press · Zbl 1009.68020
[77] Dijkstra, Ew; Scholten, Cs, Predicate calculus and program semantics (1990), New York: Springer, New York
[78] Emerson, Ea; Clarke, Em, Using branching time temporal logic to synthesize synchronization skeletons, Sci Comput Program, 2, 3, 241-266 (1982) · Zbl 0514.68032
[79] Engelmann B (2017) Techniques for the verification of dynamically typed programs. PhD thesis, University of Oldenburg, Germany
[80] 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)
[81] Foley, M., Proof of a recursive program: Quicksort, The Computer Journal, 14, 4, 391-395 (1971) · Zbl 0231.68011
[82] Filli├Ótre, J-C, Formal proof of a program: find, Sci Comput Program, 64, 3, 332-340 (2007) · Zbl 1178.68353
[83] 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-32
[84] Furia, Carlo A.; Meyer, Bertrand; Velder, Sergey, Loop invariants, ACM Computing Surveys, 46, 3, 1-51 (2014) · Zbl 1305.68054
[85] Francez, N., Fairness (1986), New York: Springer, New York · Zbl 0602.68007
[86] Francez N (1992) Program verification. Addison-Wesley, Reading · Zbl 0820.68073
[87] German, Sm; Clarke, Em; Halpern, Jy, Reasoning about procedures as parameters in the language L4, Inf Comput, 83, 3, 265-359 (1989) · Zbl 0692.68011
[88] 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-265
[89] 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-416
[90] Grumberg, Orna; Francez, Nissim; Makowsky, Johann A.; De Roever, Willem P., A proof rule for fair termination of guarded commands, Information and Control, 66, 1-2, 83-102 (1985) · Zbl 0577.68022
[91] Gries, D.; Levin, G., Assignment and procedure call proof rules, ACM Trans Program Lang Syst, 2, 4, 564-579 (1980) · Zbl 0468.68006
[92] Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. Lecture notes in computer science, vol. 78. Springer (1979)
[93] 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] Gordon MJC (1988) Programming language theory and its implementation-applicative and imperative paradigms. Prentice Hall International series in Computer Science. Prentice Hall
[95] Gries, D., The Multiple Assignment Statement, IEEE Transactions on Software Engineering, SE-4, 2, 89-93 (1978) · Zbl 0381.68017
[96] Gries, David, The Science of Programming (1981), New York, NY: Springer New York, New York, NY · Zbl 0472.68003
[97] Harel D (1979) First-order dynamic logic. Lecture notes in computer science 68. Springer, New York
[98] Hooman, Jozef; De Roever, Willem-P., The quest goes on: A survey of proofsystems for partial correctness of CSP, Current Trends in Concurrency, 343-395 (1986), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0597.68024
[99] 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-303
[100] Harel, David; Kozen, Dexter; Tiuryn, Jerzy, Dynamic Logic (2000)
[101] Hoare, Car; Lauer, Pe, Consistent and complementary formal theories of the semantics of programming languages, Acta Inform, 3, 135-153 (1974) · Zbl 0264.68006
[102] Haslbeck, Maximilian P. L.; Nipkow, Tobias, Hoare Logics for Time Bounds, Tools and Algorithms for the Construction and Analysis of Systems, 155-171 (2018), Cham: Springer International Publishing, Cham · Zbl 1423.68098
[103] Hoare, Car, Algorithm 64: quicksort, Commun ACM, 4, 7, 321 (1961)
[104] Hoare, C. A. R., An axiomatic basis for computer programming, Communications of the ACM, 12, 10, 576-580 (1969) · Zbl 0179.23105
[105] Hoare, C. A. R., Procedures and parameters: An axiomatic approach, Lecture Notes in Mathematics, 102-116 (1971), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0221.68020
[106] Hoare, Car, Proof of a program: FIND, Commun ACM, 14, 1, 39-45 (1971) · Zbl 0217.53701
[107] 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-16
[108] Hoare, Car, Proof of a structured program: ’the sieve of Eratosthenes’, Comput J, 15, 4, 321-325 (1972) · Zbl 0267.68005
[109] Hoare, C. A. R., Towards a Theory of Parallel Programming, The Origin of Concurrent Programming, 231-244 (1972), New York, NY: Springer New York, New York, NY
[110] Hoare, Car, Parallel programming: an axiomatic approach. Comput Lang, 1, 2, 151-160 (1975) · Zbl 0362.68045
[111] Hoare, Car, Communicating sequential processes. Commun ACM, 21, 666-677 (1978) · Zbl 0383.68028
[112] 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) · Zbl 1284.68400
[113] 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) · Zbl 1444.68018
[114] Hoare, Car; Wirth, N., An axiomatic definition of the programming language PASCAL, Acta Inform, 2, 335-355 (1973) · Zbl 0261.68040
[115] Limited, I.N.M.O.S.: Occam programming manual. Prentice-Hall International, Englewood Cliffs (1984)
[116] Jones CB (1981) Developing methods for computer programs including a notion of interference. PhD thesis, University of Oxford, UK
[117] Jones, Cb, Tentative steps toward a development method for interfering programs, ACM Trans Program Lang Syst, 5, 4, 596-619 (1983) · Zbl 0517.68032
[118] Jones, Cb, The early search for tractable ways of reasoning about programs, IEEE Ann Hist Comput, 25, 2, 26-49 (2003)
[119] 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-153
[120] 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-32 · Zbl 1198.68001
[121] Jensen, K., Wirth, N.: PASCAL user manual and report. Springer (1975)
[122] Kaldewaij, A.: Programming: the derivation of algorithms. Prentice-Hall International, Englewood Cliffs (1990) · Zbl 0709.68020
[123] 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) · Zbl 1444.68045
[124] King J (1969) Developing methods for computer programs including a notion of interference. PhD thesis, Department of Computer Science, Carnegie-Mellon University, Pittsburgh USA
[125] Kleymann T (1998) Hoare logic and VDM : machine-checked soundness and completeness proofs. PhD thesis, University of Edinburgh UK
[126] Kleymann, T., Hoare logic and auxiliary variables, Formal Asp Comput, 11, 5, 541-566 (1999) · Zbl 0978.03026
[127] Kozen, D., On Hoare logic and Kleene algebra with tests, ACM Trans Comput Log, 1, 1, 60-76 (2000) · Zbl 1365.68326
[128] Kozen, D.; Tiuryn, J., On the completeness of propositional Hoare logic, Inf Sci, 139, 3-4, 187-195 (2001) · Zbl 0996.03022
[129] Lamport, L., Proving the Correctness of Multiprocess Programs, IEEE Transactions on Software Engineering, SE-3, 2, 125-143 (1977) · Zbl 0349.68006
[130] Lamport, L., The temporal logic of actions, ACM Trans Program Lang Syst, 16, 3, 872-923 (1994)
[131] Lamport, L.: Specifying systems, the TLA+ language and tools for hardware and software engineers. Addison-Wesley (2002)
[132] 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, Germany
[133] Langmaack, H., On the termination problem for finitely interpreted ALGOL-like programs, Acta Inform, 18, 79-108 (1982) · Zbl 0478.68013
[134] Lauer PE (1971) Consistent formal theories of the semantics of programming languages. Technical report 25. 121, IBM Laboratory Vienna
[135] Leavens, Gt; Cheon, Y.; Clifton, C.; Ruby, C.; Cok, Dr, How the design of JML accommodates both runtime assertion checking and formal verification, Sci Comput Program, 55, 1-3, 185-208 (2005) · Zbl 1075.68009
[136] 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-370
[137] Levin, G.; Gries, D., A proof technique for communicating sequential processes, Acta Inform, 15, 281-302 (1981) · Zbl 0463.68034
[138] London, Rl; Guttag, Jv; Horning, Jj; Lampson, Bw; Mitchell, Jg; Popek, Gj, Proof rules for the programming language Euclid, Acta Inform, 10, 1-26 (1978) · Zbl 0385.68009
[139] Lipton, Rj, Reduction: a method of proving properties of parallel programs, Commun ACM, 18, 717-721 (1975) · Zbl 0316.68015
[140] 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-6
[141] 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) · Zbl 0441.68008
[142] Lehmann, D.; Pnueli, A.; Stavi, J., Impartiality, justice and fairness: The ethics of concurrent termination, Automata, Languages and Programming, 264-277 (1981), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg · Zbl 0468.68026
[143] Loeckx, J.; Sieber, K., The foundation of program verification, 2nd edn (1987), Stuttgart: Teubner-Wiley, Stuttgart
[144] Manna Z (1974) Mathematical theory of computation. Mc Graw-Hill · Zbl 0353.68066
[145] Meyer B (1997) Object-oriented software construction, 2nd edn. Prentice Hall · Zbl 0987.68516
[146] Milner R (1980) A calculus of communicating systems. Lecture notes in computer science 92, Springer, New York
[147] Milner, R., Communication and concurrency (1989), Englewood Cliffs: Prentice-Hall International, Englewood Cliffs
[148] Morris, Fl; Jones, Cb, An early program proof by Alan Turing, Ann Hist Comput, 6, 139-143 (1984) · Zbl 0998.01521
[149] McIver A, Morgan C (2005) Abstraction, refinement and proof for probabilistic systems. Monographs in computer science. Springer · Zbl 1069.68039
[150] Moitra, A., On Apt, Francez, and de Roever’s “A proof system for communicating sequential processes”, ACM TransProgram Lang Syst, 5, 3, 500-501 (1983)
[151] Morgan C (1994) Programming from specifications, 2nd end. Prentice-Hall International, London
[152] Manna, Z.; Pnueli, A., Axiomatic approach to total correctness of programs, Acta Inform, 3, 253-263 (1974) · Zbl 0263.68009
[153] Manna, Z.; Pnueli, A., The temporal logic of reactive andconcurrent systems-specification (1991), New York: Springer, New York
[154] Manna, Z.; Pnueli, A., Temporal verification of reactive systems-safety (1995), New York: Springer, New York
[155] Mirkowska, C.; Salwicki, A., Algorithmic logic (1987), Norwell: Kluwer Academic Publishers, Norwell · Zbl 0648.03018
[156] Naur, P., Proof of algorithms by general snapshots, BIT Numer Math, 6, 4, 310-316 (1966)
[157] 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-453
[158] Nordio, Martin; Calcagno, Cristiano; Müller, Peter; Meyer, Bertrand, A Sound and Complete Program Logic for Eiffel, Objects, Components, Models and Patterns, 195-214 (2009), Berlin, Heidelberg: Springer Berlin Heidelberg, Berlin, Heidelberg
[159] Nielson, Hr, A Hoare-like proof system for analysing the computation time of programs, Sci Comput Program, 9, 2, 107-136 (1987) · Zbl 0622.68026
[160] 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-367
[161] 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-119
[162] 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)
[163] 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) · Zbl 0994.68131
[164] Olderog, E-R; Apt, Kr, Fairness in parallel programs, the transformational approach, ACM Trans Program Lang Syst, 10, 420-455 (1988)
[165] Owicki, S.; Gries, D., An axiomatic proof technique for parallel programs, Acta Inform, 6, 319-340 (1976) · Zbl 0312.68011
[166] Owicki, S.; Gries, D., Verifying properties of parallel programs: an axiomatic approach, Commun ACM, 19, 279-285 (1976) · Zbl 0322.68010
[167] O’Hearn, Pw, Resources, concurrency, and local reasoning, Theor Comput Sci, 375, 1-3, 271-307 (2007) · Zbl 1111.68023
[168] O’Hearn, Pw, Separation logic, Commun ACM, 62, 2, 86-95 (2019)
[169] Olderog, E-R, Sound and complete Hoare-like calculi based on copy rules, Acta Inform, 16, 161-197 (1981) · Zbl 0464.68037
[170] 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-329
[171] Olderog, E-R, On the notion of expressiveness and the rule of adaptation, Theor Comput Sci, 30, 337-347 (1983) · Zbl 0511.68006
[172] Olderog, E-R, Correctness of programs with Pascal-like procedures without global variables, Theor Comput Sci, 30, 49-90 (1984) · Zbl 0557.90107
[173] 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) · Zbl 1274.68035
[174] 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)
[175] 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)
[176] Olderog, E-R; Wilhelm, R., Turing und die Verifikation, Informatik Spektrum, 35, 4, 271-279 (2012)
[177] Owicki S (1975) Axiomatic proof techniques for parallel programs. Outstanding dissertations in the computer sciences. Garland Publishing, New York
[178] Owicki S (1976) A consistent and complete deductive system for theverification of parallel programs. In: STOC. ACM, pp 73-86
[179] 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-298
[180] 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-280
[181] 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-78 · Zbl 1253.68087
[182] Platzer, A., Differential dynamic logic for hybrid systems, J Autom Reasoning, 41, 2, 143-189 (2008) · Zbl 1181.03035
[183] Pnueli A (1977) The temporal logic of programs. In: Proceedings of the 18th IEEE symposium on foundations of computer science, pp46-57
[184] Piskac, Ruzica; Rümmer, Philipp, Verified Software. Theories, Tools, and Experiments (2018), Cham: Springer International Publishing, Cham · Zbl 1400.68034
[185] 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-121
[186] Queille JP, Sifakis J (1981) Specification and verification of concurrent systems in CESAR. In: Proceedings of the 5th international symposium on programming, Paris · Zbl 0482.68028
[187] 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-74
[188] Salwicki, A., Formalized algorithmic languages. Bull Acad Pol Sci, 18, 227-232 (1970) · Zbl 0198.02801
[189] Schwarz, J., Generic commands-a tool for partial correctness formalisms, Comput J, 20, 151-155 (1977) · Zbl 0359.68012
[190] 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-483
[191] Sokołowski, S., Soundness of Hoare’s logic: an automated proof using LCF, ACM Trans Program Lang Syst, 9, 1, 100-120 (1987)
[192] Spivey JM (1992) The Z notation: a reference manual, 2nd edn. Prentice Hall
[193] 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-346
[194] Tarski, A., Der Wahrheitsbegriff in den formalisierten Sprachen, Studia Philosophica, 1, 3, 261-405 (1936)
[195] 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)
[196] Tucker, Jv; Zucker, Ji, Program correctness over abstract datatypes, with error-state semantics (1988), Amsterdam: North-Holland and CWI Monographs, Amsterdam
[197] Unruh, Dominique, Quantum relational Hoare logic, Proceedings of the ACM on Programming Languages, 3, POPL, 1-31 (2019)
[198] 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-180 · Zbl 0956.68086
[199] 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-105 · Zbl 1064.68543
[200] Van Wijngaarden, A.; Mailloux, Bj; Peck, Jel; Koster, Cha; Sintzoff, M.; Lindsey, Ch; Meertens, Lglt; Fisker, Rg, Revised report on the algorithmic language ALGOL 68, Acta Inform, 5, 1-236 (1975) · Zbl 0317.68007
[201] Wand, M., A new incompleteness result for Hoare’s system, JACM, 25, 1, 168-175 (1978) · Zbl 0364.68008
[202] Wirth, N.; Hoare, Car, A contribution to the development of ALGOL, Commun ACM, 9, 6, 413-432 (1966) · Zbl 0143.18603
[203] Winskel, G., The formal semantics of programming languages-an introduction (1993), Foundation of computing series: MIT Press, Foundation of computing series
[204] Ying, Mingsheng, Floyd-hoare logic for quantum programs, ACM Transactions on Programming Languages and Systems, 33, 6, 1-49 (2011)
[205] Ying, M., Toward automatic verification of quantum programs, Formal Asp Comput, 31, 1, 3-25 (2019) · Zbl 1425.68271
[206] Zöbel, D., Normalform-Transformationen für CSP-Programme. Informatik: Forschung und Entwicklung, 3, 64-76 (1988) · Zbl 0646.68032
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.