# FAQs About K and Matching Logic

(back to Grigore Rosu's webpage) (back to the Programming Language Design and Semantics webpage)

This page is under heavy construction. Right now we are collecting the questions to be addressed. Please let us know (grosu@illinois.edu) if your questions are not among the ones below.

Is there a (preferably short) paper that overviews the K and matching logic approach? |
---|

Try this one, which also explains the high-level connection to rewriting logic:

**From Rewriting Logic, to Programming Language Semantics, to Program Verification**- Grigore Rosu
, LNCS 9200, pp 598-616. 2015**Meseguer's Festschrift**

*Abstract.*Rewriting logic has proven to be an excellent formalism to define executable semantics of programming languages, concurrent or not, and then to derive formal analysis tools for the defined languages with very little effort, such as model checkers. In this paper we give an overview of recent results obtained in the context of the rewriting logic semantics framework K, such as complete semantics of large programming languages like C, Java, JavaScript, Python, and deductive program verification techniques that allow us to verify programs in these languages using a common verification infrastructure.

What are the most relevant papers that I should read? |
---|

...

Are there other similar overview papers? |
---|

...

When and how was K invented? |
---|

Unlike other semantic frameworks, K was not invented. It was engineered. We have systematically studied ...

When and how was matching logic invented? |
---|

...

When and how was reachability logic invented? |
---|

...

I want a complete reading list of all papers written on this topic, in chronological order. |
---|

...

Can you briefly tell me what is K? |
---|

...

Can you briefly tell me what is matching logic? |
---|

...

What is the current (as of 2016) state-of-the-art and why do you think your approach is better? |
---|

...

What is the difference between matching logic and reachability logic? |
---|

...

What is the difference between K and rewrite logic? |
---|

...

What is the difference between K and small-step structural operational semantics? |
---|

...

What is the difference between K and reduction semantics with evaluation contexts? |
---|

...

The hardest part of program verification is to find and reason about state abstractions. How do you address that? |
---|

...

What is the difference between defining a language in K and translating a language to K? |
---|

...

Can you do language translations in K? |
---|

...

How is your approach different from translating my language to an IVL, say Boogie, or Why, or LLVM? |
---|

...

What is the difference between matching logic and separation logic? |
---|

Separation logic is a compact notation for first-order logic in a particular model, that of maps.
Matching logic is also a notation for first-order logic, but it is not restricted to any particular model.
When picking the same model of maps that is hardwired in separation logic, and a syntax for patterns that resembles the separation logic syntax, then the resulting matching logic instance becomes *exactly* separation logic, both in terms of syntax and in terms of validity/satisfiability.
Matching logic, however, has the advantage that it is not restricted to any particular model, which turned out to be a very important aspect in practice.
While in separation-logic-based verification approaches you have to either translate your language properties to separation logic or to extend separation logic with particular constructs that are important for your language (e.g., with "concurrency", or with "stacks", etc.), when using matching logic you have to neither touch the logic itself nor translate your assertions to it.
That's because matching logic is powerful enough to express any semantic components that you need for your language.
In terms of separation, you can think of matching logic as a sort of "parametric" separation logic, that gets automatically instantiated for your language of interest once you define your language's configurations.
In doing so, it gives you separation at all levels in your program configuration, not only in the heap.
Of course, like with any other logic that is used for program reasoning, you may need to define abstractions in order to specify and/or verify what you want, but in matching logic those can be defined using its usual sentences/patterns, without any special extensions (e.g., "recursive predicates"), again because it is powerful enough to let you do that. See the following paper for a high-level presentation of matching logic:

**Matching Logic --- Extended Abstract**- Grigore Rosu
, Leibniz International Proceedings in Informatics (LIPIcs) 36, pp 5-21. 2015**RTA'15**

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

How is your approach more economical than the state-of-the-art? |
---|

...