Matching logic: a new program verification approach.
Grigore Roşu, Andrei R Stefanescu · International Conference on Software Engineering · 2011
Matching logic is a new program verication logic, which builds upon operational semantics. Matching logic specications are constrained symbolic program congurations, called patterns, which can be matched by concrete congurations. By building upon an operational semantics of the language and allowing specications to directly refer to the structure of the conguration, matching logic has at least three benets that could be key factors in its usability: (1) One’s familiarity with the formalism reduces to one’s familiarity with the operational semantics of the language, that is, with the language itself; (2) The verication process proceeds the same way as the execution of the program, making debugging failed proof attempts manageable because one can always see the \current and \what went wrong, same like in a debugger; and (3) Nothing is lost in translation, that is, there is no gap between the language itself and its verier. Moreover, direct access to the structure of the conguration facilitates dening sub-patterns that one may reason about, such as disjoint lists or trees in the heap, as well as supporting framing in various components of the conguration at no additional costs.