Skip to main content
SpringerLink
Log in

Matching Logic: An Alternative to Hoare/Floyd Logic

  • Conference paper
Book cover Algebraic Methodology and Software Technology (AMAST 2010)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 6486))

Abstract

This paper introduces matching logic, a novel framework for defining axiomatic semantics for programming languages, inspired from operational semantics. Matching logic specifications are particular first-order formulae with constrained algebraic structure, called patterns. Program configurations satisfy patterns iff they match their algebraic structure and satisfy their constraints. Using a simple imperative language (IMP), it is shown that a restricted use of the matching logic proof system is equivalent to IMP’s Hoare logic proof system, in that any proof derived using either can be turned into a proof using the other. Extensions to IMP including a heap with dynamic memory allocation and pointer arithmetic are given, requiring no extension of the underlying first-order logic; moreover, heap patterns such as lists, trees, queues, graphs, etc., are given algebraically using fist-order constraints over patterns.

Supported in part by NSF grants CCF-0916893, CNS-0720512, and CCF-0448501, by NASA contract NNL08AA23C, by a Samsung SAIT grant, and by several Microsoft gifts.

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 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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  2. Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)

    Google Scholar 

  3. Berdine, J., Calcagno, C., O’Hearn, P.W.: Symbolic execution with separation logic. In: Yi, K. (ed.) APLAS 2005. LNCS, vol. 3780, pp. 52–68. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  4. Clavel, M., Durán, F., Eker, S., Meseguer, J., Lincoln, P., Martí-Oliet, N., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)

    MATH  Google Scholar 

  5. Cohen, E., Moskal, M., Schulte, W., Tobies, S.: A practical verification methodology for concurrent programs. Tech. Rep. MSR-TR-2009-15, Microsoft Research (2009)

    Google Scholar 

  6. Distefano, D., O’Hearn, P.W., Yang, H.: A local shape analysis based on separation logic. In: Hermanns, H., Palsberg, J. (eds.) TACAS 2006. LNCS, vol. 3920, pp. 287–302. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  7. Distefano, D., Parkinson, M.J.: jStar: Towards practical verification for Java. In: OOPSLA 2008, pp. 213–226 (2008)

    Google Scholar 

  8. Filliâtre, J.C., Marché, C.: The Why/Krakatoa/Caduceus platform for deductive program verification. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 173–177. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  9. Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: PLDI 2002, pp. 234–245 (2002)

    Google Scholar 

  10. Floyd, R.W.: Assigning meaning to programs. In: Schwartz, J.T. (ed.) Proceedings of the Symposium on Applied Mathematics, 19th edn., pp. 19–32. AMS, Providence (1967)

    Google Scholar 

  11. Goguen, J., Malcolm, G.: Algebraic Semantics of Imperative Programs. MIT Press, Cambridge (1996)

    MATH  Google Scholar 

  12. Gordon, M., Collavizza, H.: Forward with Hoare. In: Reflections on the Work of C.A.R. Hoare. History of Computing Series, Springer, Heidelberg (2010)

    Google Scholar 

  13. Gries, D.: The Schorr-Waite graph marking algorithm. Acta Informatica 11, 223–232 (1979)

    Article  MATH  Google Scholar 

  14. Harel, D., Kozen, D., Tiuryn, J.: Dynamic logic. In: Handbook of Philosophical Logic, pp. 497–604 (1984)

    Google Scholar 

  15. Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12(10), 576–580 (1969)

    Article  MATH  Google Scholar 

  16. Hubert, T., Marché, C.: A case study of C source code verification: The Schorr-Waite algorithm. In: SEFM 2005, pp. 190–199 (2005)

    Google Scholar 

  17. Lahiri, S.K., Qadeer, S.: Verifying properties of well-founded linked lists. In: POPL 2006, pp. 115–126 (2006)

    Google Scholar 

  18. Lev-Ami, T., Immerman, N., Reps, T., Sagiv, M., Srivastava, S.: Simulating reachability using first-order logic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 99–115. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  19. Loginov, A., Reps, T., Sagiv, M.: Automated verification of the Deutsch-Schorr-Waite tree-traversal algorithm. In: Yi, K. (ed.) SAS 2006. LNCS, vol. 4134, pp. 261–279. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  20. Meseguer, J., Roşu, G.: The rewriting logic semantics project. Theoretical Computer Science 373(3), 213–237 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  21. Møller, A., Schwartzbach, M.I.: The pointer assertion logic engine. SIGPLAN Not. 36(5), 221–231 (2001)

    Article  Google Scholar 

  22. Nipkow, T.: Winskel is (almost) right: Towards a mechanized semantics. Formal Aspects of Computing 10(2), 171–186 (1998)

    Article  MATH  Google Scholar 

  23. O’Hearn, P.W., Pym, D.J.: The logic of bunched implications. Bulletin of Symbolic Logic 5, 215–244 (1999)

    Article  MathSciNet  MATH  Google Scholar 

  24. Pavlovic, D., Smith, D.R.: Composition and refinement of behavioral specifications. In: ASE 2001, pp. 157–165 (2001)

    Google Scholar 

  25. Reynolds, J.C.: Separation logic: A logic for shared mutable data structures. In: LICS 2002, pp. 55–74 (2002)

    Google Scholar 

  26. Roşu, G., Schulte, W.: Matching logic–Extended report. Tech. Rep. UIUCDCS-R-2009-3026, University of Illinois (2009)

    Google Scholar 

  27. Roşu, G., Ellison, C., Schulte, W.: From rewriting logic executable semantics to matching logic program verification. Tech. Rep. UIUC (2009), http://hdl.handle.net/2142/13159

  28. Roşu, G., Şerbănuţă, T.F.: An overview of the K semantic framework. Journal of Logic and Algebraic Programming 79(6), 397–434 (2010)

    Article  MathSciNet  MATH  Google Scholar 

  29. Sagiv, M., Reps, T., Wilhelm, R.: Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems 24(3), 217–298 (2002)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. University of Illinois, Urbana-Champaign, USA

    Grigore Roşu & Chucky Ellison

  2. Microsoft Research, Redmond, USA

    Wolfram Schulte

Authors
  1. Grigore Roşu
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Chucky Ellison
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Wolfram Schulte
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Macquarie University, Sydney, Australia

    Michael Johnson

  2. University of Oxford, Oxford, UK

    Dusko Pavlovic

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Roşu, G., Ellison, C., Schulte, W. (2011). Matching Logic: An Alternative to Hoare/Floyd Logic. In: Johnson, M., Pavlovic, D. (eds) Algebraic Methodology and Software Technology. AMAST 2010. Lecture Notes in Computer Science, vol 6486. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17796-5_9

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17796-5_9

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17795-8

  • Online ISBN: 978-3-642-17796-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation