Skip to main content
SpringerLink
Log in

Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles (ISoLA 2020)

We’re sorry, something doesn't seem to be working properly.

Please try refreshing the page. If that doesn't work, please contact support so we can address the problem.

Included in the following conference series:

Abstract

Relational Hoare logics extend the applicability of modular, deductive verification to encompass important 2-run properties including dependency requirements such as confidentiality and program relations such as equivalence or similarity between program versions. A considerable number of recent works introduce different relational Hoare logics without yet converging on a core set of proof rules. This paper looks backwards to little known early work. This brings to light some principles that clarify and organize the rules as well as suggesting a new rule and a new notion of completeness.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. Aguirre, A., Barthe, G., Gaboardi, M., Garg, D., Strub, P.: A relational logic for higher-order programs. J. Funct. Program. 29, e16 (2019). https://doi.org/10.1017/S0956796819000145

    Article  MathSciNet  Google Scholar 

  2. Apt, K.: Ten years of Hoare’s logic, a survey, part I. ACM Trans. Program. Lang. Syst. 3(4), 431–483 (1981)

    Article  Google Scholar 

  3. Apt, K.: Ten years of Hoare’s logic, a survey, part II: nondeterminism. Theor. Comput. Sci. 28, 83–109 (1984)

    Article  Google Scholar 

  4. Apt, K.R.: Correctness proofs of distributed termination algorithms. ACM Trans. Program. Lang. Syst. 8, 388–405 (1986)

    Article  Google Scholar 

  5. Apt, K.R., de Boer, F.S., Olderog, E.R.: Verification of Sequential and Concurrent Programs, 3rd edn. Springer, Heidelberg (2009). https://doi.org/10.1007/978-1-84882-745-5

    Book  MATH  Google Scholar 

  6. Apt, K.R., Olderog, E.: Fifty years of Hoare’s logic. Formal Asp. Comput. 31(6), 751–807 (2019)

    Article  MathSciNet  Google Scholar 

  7. Banerjee, A., Naumann, D.A.: Ownership confinement ensures representation independence for object-oriented programs. J. ACM 52(6), 894–960 (2005)

    Article  MathSciNet  Google Scholar 

  8. Banerjee, A., Naumann, D.A.: Local reasoning for global invariants, part II: dynamic boundaries. J. ACM 60(3), 19:1–19:73 (2013)

    Article  MathSciNet  Google Scholar 

  9. Banerjee, A., Naumann, D.A., Nikouei, M.: Relational logic with framing and hypotheses. In: Foundations of Software Technology and Theoretical Computer Science, pp. 11:1–11:16 (2016). Technical report at http://arxiv.org/abs/1611.08992

  10. Banerjee, A., Naumann, D.A., Nikouei, M.: A logical analysis of framing for specifications with pure method calls. ACM Trans. Program. Lang. Syst. 40(2), 6:1–6:90 (2018)

    Article  Google Scholar 

  11. Barthe, G., Crespo, J.M., Kunz, C.: Relational verification using product programs. In: Butler, M., Schulte, W. (eds.) FM 2011. LNCS, vol. 6664, pp. 200–214. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-21437-0_17

    Chapter  Google Scholar 

  12. Barthe, G., Crespo, J.M., Kunz, C.: Beyond 2-safety: asymmetric product programs for relational program verification. In: Artemov, S., Nerode, A. (eds.) LFCS 2013. LNCS, vol. 7734, pp. 29–43. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35722-0_3

    Chapter  Google Scholar 

  13. Barthe, G., Crespo, J.M., Kunz, C.: Product programs and relational program logics. J. Logical Algebraic Methods Program. 85(5), 847–859 (2016)

    Article  MathSciNet  Google Scholar 

  14. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. In: IEEE CSFW, pp. 100–114 (2004). See extended version [15]

    Google Scholar 

  15. Barthe, G., D’Argenio, P.R., Rezk, T.: Secure information flow by self-composition. Math. Struct. Comput. Sci. 21(6), 1207–1252 (2011)

    Article  MathSciNet  Google Scholar 

  16. Barthe, G., Grégoire, B., Hsu, J., Strub, P.: Coupling proofs are probabilistic product programs. In: POPL, pp. 161–174 (2017)

    Google Scholar 

  17. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-69061-0

    Book  Google Scholar 

  18. Beckert, B., Ulbrich, M.: Trends in relational program verification. In: Müller, P., Schaefer, I. (eds.) Principled Software Development, pp. 41–58. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-98047-8_3

    Chapter  Google Scholar 

  19. Benton, N.: Simple relational correctness proofs for static analyses and program transformations. In: POPL, pp. 14–25 (2004)

    Google Scholar 

  20. Beringer, L.: Relational decomposition. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 39–54. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-22863-6_6

    Chapter  Google Scholar 

  21. Beringer, L., Hofmann, M.: Secure information flow and program logics. In: IEEE CSF, pp. 233–248 (2007)

    Google Scholar 

  22. Churchill, B.R., Padon, O., Sharma, R., Aiken, A.: Semantic program alignment for equivalence checking. In: PLDI, pp. 1027–1040 (2019)

    Google Scholar 

  23. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)

    Article  Google Scholar 

  24. Clochard, M., Marché, C., Paskevich, A.: Deductive verification with ghost monitors. Proc. ACM Program. Lang. 4(POPL), 2:1–2:26 (2020)

    Article  Google Scholar 

  25. Cok, D.R.: Reasoning with specifications containing method calls and model fields. J. Object Technol. 4(8), 77–103 (2005)

    Article  Google Scholar 

  26. Csirmaz, L.: Program correctness on finite fields. Periodica Mathematica Hungarica 33(1), 23–33 (1996)

    Article  MathSciNet  Google Scholar 

  27. Csirmaz, L., Hart, B.: Program correctness on finite fields. In: IEEE Symposium on Logic in Computer Science (LICS), pp. 4–10 (1986). See also [26]

    Google Scholar 

  28. Darvas, Á., Hähnle, R., Sands, D.: A theorem proving approach to analysis of secure information flow. In: Hutter, D., Ullmann, M. (eds.) SPC 2005. LNCS, vol. 3450, pp. 193–209. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-32004-3_20

    Chapter  Google Scholar 

  29. Eilers, M., Müller, P., Hitz, S.: Modular product programs. ACM Trans. Program. Lang. Syst. 42(1), 3:1–3:37 (2020)

    Article  Google Scholar 

  30. Floyd, R.: Assigning meaning to programs. In: Symposium on Applied Mathematics, Mathematical Aspects of Computer Science, vol. 19, pp. 19–32. American Mathematical Society (1967)

    Google Scholar 

  31. Francez, N.: Product properties and their direct verification. Acta Inf. 20, 329–344 (1983)

    Article  MathSciNet  Google Scholar 

  32. Girka, T., Mentré, D., Régis-Gianas, Y.: Verifiable semantic difference languages. In: Principles and Practice of Declarative Programming (PPDP) (2017)

    Google Scholar 

  33. Godlin, B., Strichman, O.: Inference rules for proving the equivalence of recursive procedures. Acta Inf. 45(6), 403–439 (2008)

    Article  MathSciNet  Google Scholar 

  34. Grimm, N., et al.: A monadic framework for relational verification: applied to information security, program equivalence, and optimizations. In: CPP (2018)

    Google Scholar 

  35. Hawblitzel, C., Kawaguchi, M., Lahiri, S.K., Rebêlo, H.: Towards modularly comparing programs using automated theorem provers. In: Bonacina, M.P. (ed.) CADE 2013. LNCS (LNAI), vol. 7898, pp. 282–299. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38574-2_20

    Chapter  MATH  Google Scholar 

  36. Hoare, C.A.R.: Procedures and parameters: an axiomatic approach. In: Engeler, E. (ed.) Symposium on Semantics of Algorithmic Languages. LNM, vol. 188, pp. 102–116. Springer, Heidelberg (1971). https://doi.org/10.1007/BFb0059696

    Chapter  Google Scholar 

  37. Hoare, C.A.R., He, J.: The weakest prespecification. Inf. Process. Lett. 24(2), 127–132 (1987)

    Article  MathSciNet  Google Scholar 

  38. Kiefer, M., Klebanov, V., Ulbrich, M.: Relational program reasoning using compiler IR: combining static verification and dynamic analysis. J. Autom. Reason. 60, 337–363 (2018)

    Article  MathSciNet  Google Scholar 

  39. Kleymann, T.: Hoare logic and auxiliary variables. Formal Aspects Comput. 11, 541–566 (1999)

    Article  Google Scholar 

  40. Lahiri, S.K., Hawblitzel, C., Kawaguchi, M., Rebêlo, H.: SYMDIFF: a language-agnostic semantic diff tool for imperative programs. In: Madhusudan, P., Seshia, S.A. (eds.) CAV 2012. LNCS, vol. 7358, pp. 712–717. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-31424-7_54

    Chapter  Google Scholar 

  41. Lahiri, S.K., McMillan, K.L., Sharma, R., Hawblitzel, C.: Differential assertion checking. In: Joint Meeting of the European Software Engineering Conference and the ACM Symposium on the Foundations of Software Engineering (2013)

    Google Scholar 

  42. Lahiri, S.K., Murawski, A.S., Strichman, O., Ulbrich, M.: Program equivalence (Dagstuhl Seminar 18151). Dagstuhl Rep. 8(4), 1–19 (2018)

    Google Scholar 

  43. Leino, K.R.M.: Dafny: an automatic program verifier for functional correctness. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 348–370. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-17511-4_20

    Chapter  MATH  Google Scholar 

  44. Maillard, K., Hritçu, C., Rivas, E., Muylder, A.V.: The next 700 relational program logics. Proc. ACM Program. Lang. 4(POPL), 4:1–4:33 (2020)

    Article  Google Scholar 

  45. Moore, J.S.: Inductive assertions and operational semantics. Int. J. Softw. Tools Technol. Transf. 8(4–5), 359–371 (2006)

    Article  Google Scholar 

  46. Morgan, C.: Auxiliary variables in data refinement. Inf. Process. Lett. 29(6), 293–296 (1988)

    Article  MathSciNet  Google Scholar 

  47. Müller, C., Kovács, M., Seidl, H.: An analysis of universal information flow based on self-composition. In: IEEE CSF (2015)

    Google Scholar 

  48. Namjoshi, K.S., Singhania, N.: Loopy: programmable and formally verified loop transformations. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 383–402. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_19

    Chapter  Google Scholar 

  49. Nanevski, A., Banerjee, A., Garg, D.: Verification of information flow and access control policies with dependent types. In: IEEE Symposium on Security and Privacy (2011)

    Google Scholar 

  50. Naumann, D.A.: Calculating sharp adaptation rules. Inf. Process. Lett. 77, 201–208 (2001)

    Article  MathSciNet  Google Scholar 

  51. Naumann, D.A.: From coupling relations to mated invariants for secure information flow. In: ESORICS. LNCS, vol. 4189, pp. 279–296 (2006)

    Google Scholar 

  52. Nikouei, M., Banerjee, A., Naumann, D.A.: Data abstraction and relational program logic. CoRR abs/1910.14560 (2019). http://arxiv.org/abs/1910.14560

  53. O’Hearn, P., Reynolds, J., Yang, H.: Local reasoning about programs that alter data structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 1–19. Springer, Heidelberg (2001). https://doi.org/10.1007/3-540-44802-0_1

    Chapter  Google Scholar 

  54. O’Hearn, P.W., Yang, H., Reynolds, J.C.: Separation and information hiding. ACM Trans. Program. Lang. Syst. 31(3), 1–50 (2009)

    Article  Google Scholar 

  55. Olderog, E.R.: On the notion of expressiveness and the rule of adaptation. Theor. Comput. Sci. 30, 337–347 (1983)

    Article  MathSciNet  Google Scholar 

  56. Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs I. Acta Inf. 6, 319–340 (1976)

    Article  MathSciNet  Google Scholar 

  57. Pick, L., Fedyukovich, G., Gupta, A.: Exploiting synchrony and symmetry in relational verification. In: Chockler, H., Weissenbacher, G. (eds.) CAV 2018. LNCS, vol. 10981, pp. 164–182. Springer, Cham (2018). https://doi.org/10.1007/978-3-319-96145-3_9

    Chapter  Google Scholar 

  58. Reynolds, J.C.: The Craft of Programming. Prentice-Hall, Upper Saddle River (1981)

    MATH  Google Scholar 

  59. de Roever, W.P., Engelhardt, K.: Data Refinement: Model-Oriented Proof Methods and their Comparison. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

  60. Shemer, R., Gurfinkel, A., Shoham, S., Vizel, Y.: Property directed self composition. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 161–179. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_9

    Chapter  Google Scholar 

  61. Sousa, M., Dillig, I.: Cartesian Hoare Logic for verifying k-safety properties. In: PLDI, pp. 57–69 (2016)

    Google Scholar 

  62. Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005). https://doi.org/10.1007/11547662_24

    Chapter  Google Scholar 

  63. Wood, T., Drossopolou, S., Lahiri, S.K., Eisenbach, S.: Modular verification of procedure equivalence in the presence of memory allocation. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 937–963. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54434-1_35

    Chapter  Google Scholar 

  64. Yang, H.: Relational separation logic. Theor. Comput. Sci. 375, 308–334 (2007)

    Article  MathSciNet  Google Scholar 

  65. Zaks, A., Pnueli, A.: CoVaC: compiler validation by program analysis of the cross-product. In: Cuellar, J., Maibaum, T., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 35–51. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68237-0_5

    Chapter  Google Scholar 

Download references

Acknowledgments

The paper was improved thanks to comments from Krzysztof Apt, Anindya Banerjee, Gilles Barthe, Ramana Nagasamudram, and anonymous reviewers. The research was partially supported by NSF CNS 1718713 and ONR N00014-17-1-2787.

Author information

Authors and Affiliations

  1. Stevens Institute of Technology, Hoboken, USA

    David A. Naumann

Authors
  1. David A. Naumann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to David A. Naumann .

Editor information

Editors and Affiliations

  1. University of Limerick and Lero, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Naumann, D.A. (2020). Thirty-Seven Years of Relational Hoare Logic: Remarks on Its Principles and History. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation: Engineering Principles. ISoLA 2020. Lecture Notes in Computer Science(), vol 12477. Springer, Cham. https://doi.org/10.1007/978-3-030-61470-6_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-61470-6_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-61469-0

  • Online ISBN: 978-3-030-61470-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation