Document Open Access Logo

Matching Logic - Extended Abstract (Invited Talk)

Author Grigore Rosu

PDF
Thumbnail PDF

File

LIPIcs.RTA.2015.5.pdf
  • Filesize: 0.56 MB
  • 17 pages

Document Identifiers

Author Details

Grigore Rosu

Cite AsGet BibTex

Grigore Rosu. Matching Logic - Extended Abstract (Invited Talk). In 26th International Conference on Rewriting Techniques and Applications (RTA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 36, pp. 5-21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015)
https://doi.org/10.4230/LIPIcs.RTA.2015.5

Abstract

This paper presents matching logic, a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the patterns, are constructed using variables, symbols, connectives and quantifiers, but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that match it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have a rewrite-based operational semantics.
Keywords
  • Program logic
  • First-order logic
  • Rewriting
  • Verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Timos Antonopoulos, Nikos Gorogiannis, Christoph Haase, Max I. Kanovich, and Joël Ouaknine. Foundations for decision problems in separation logic with general inductive predicates. In FOSSACS'14, LNCS 8412, pages 411-425, 2014. Google Scholar
  2. Denis Bogdănaş and Grigore Roşu. K-Java: A Complete Semantics of Java. In POPL'15, pages 445-456. ACM, 2015. Google Scholar
  3. James Brotherston, Carsten Fuhs, Nikos Gorogiannis, and Juan Navarro Pérez. A decision procedure for satisfiability in separation logic with inductive predicates. Technical Report RN/13/15, University College London, 2013. Google Scholar
  4. Andrei Ştefănescu, Ştefan Ciobâcă, Radu Mereuţă, Brandon M. Moore, Traian Florin Şerbănuţă, and Grigore Roşu. All-path reachability logic. In RTA-TLCA'14, volume 8560 of LNCS, pages 425-440. Springer, 2014. Google Scholar
  5. Leonardo De Moura and Nikolaj Bjørner. Z3: an efficient SMT solver. In TACAS, pages 337-340, 2008. LNCS 4963. Google Scholar
  6. Chucky Ellison and Grigore Rosu. An executable formal semantics of C with applications. In POPL, pages 533-544, 2012. Google Scholar
  7. William M. Farmer and Joshua D. Guttman. A set theory with support for partial functions. Studia Logica, 66(1):59-78, 2000. Google Scholar
  8. Chris Hathhorn, Chucky Ellison, and Grigore Roşu. Defining the undefinedness of C. In PLDI'15. ACM, 2015. Google Scholar
  9. Radu Iosif, Adam Rogalewicz, and Jirí Simácek. The tree width of separation logic with recursive definitions. In CADE'13, LNCS 7898, 2013. Google Scholar
  10. C. Barry Jay. The pattern calculus. ACM Trans. Program. Lang. Syst., 26(6):911-937, November 2004. Google Scholar
  11. Peter O'Hearn, John Reynolds, and Hongseok Yang. Local reasoning about programs that alter data structures. In CSL, pages 1-19. LNCS 2142, 2001. Google Scholar
  12. Peter W. O'Hearn and David J. Pym. The logic of bunched implications. Bulletin of Symb. Logic, 5(2):215-244, 1999. Google Scholar
  13. Daejun Park, Andrei Ştefănescu, and Grigore Roşu. KJS: A complete formal semantics of JavaScript. In Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'15). ACM, 2015. Google Scholar
  14. John C. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS, pages 55-74, 2002. Google Scholar
  15. Grigore Roşu. Matching logic: A logic for structural reasoning. Technical Report http://hdl.handle.net/2142/47004, University of Illinois, Jan 2014. Google Scholar
  16. Grigore Roşu, Andrei Ştefănescu, Ştefan Ciobâcă, and Brandon M. Moore. One-path reachability logic. In LICS'13. IEEE, 2013. Google Scholar
  17. Grigore Rosu, Chucky Ellison, and Wolfram Schulte. Matching logic: An alternative to Hoare/Floyd logic. In AMAST, volume 6486 of LNCS, pages 142-162, 2010. Google Scholar
  18. Grigore Roşu and Traian Florin Şerbănuţă. An overview of the K semantic framework. Journal of Logic and Algebraic Programming, 79(6):397-434, 2010. Google Scholar
  19. Grigore Rosu and Traian Florin Serbanuta. K overview and simple case study. In Proc. of International K Workshop (K'11), volume 304 of ENTCS, pages 3-56. Elsevier, 2014. Google Scholar
  20. Grigore Rosu and Andrei Stefanescu. Checking reachability using matching logic. In OOPSLA'12, pages 555-574. ACM, 2012. Google Scholar
  21. A. Tarski and S.R. Givant. A Formalization of Set Theory Without Variables. Number 41 in Colloquium Publications. AMS, 1987. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact