Matching Logic: A New Program Verification Approach

From FSL
Jump to: navigation, search

NIER ICSE'11

Matching Logic: A New Program Verification Approach (NIER Track)
Grigore Rosu and Andrei Stefanescu
ICSE'11, ACM, pp 868-871. 2011
Abstract. Matching logic is a new program verification logic, which builds upon operational semantics. Matching logic specifications are constrained symbolic program configurations, called patterns, which can be matched by concrete configurations. By building upon an operational semantics of the language and allowing specifications to directly refer to the structure of the configuration, matching logic has at least three benefits that could be key factors in its potential 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 verification process proceeds the same way as the execution of the program, making debugging failed proof attempts manageable because one can always see the ``current configuration 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 verifier. Moreover, direct access to the structure of the configuration facilitates defining 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 configuration at no additional costs.
PDF, Slides(PPTX), Slides(PDF), Matching Logic, DOI, ICSE'11, BIB


UV'10

Matching Logic: A New Program Verification Approach
Grigore Rosu and Andrei Stefanescu
UV'10. 2010
Abstract. Matching logic is a new program verification logic, which builds upon operational semantics. Matching logic specifications are constrained symbolic program configurations, called patterns, which can be matched by concrete configurations. By building upon an operational semantics of the language and allowing specifications to directly refer to the structure of the configuration, matching logic has at least three benefits 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 verification process proceeds the same way as the execution of the program, making debugging failed proof attempts manageable because one can always see the "current configuration" 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 verifier. Moreover, direct access to the structure of the configuration facilitates defining 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 configuration at no additional costs.
PDF, Slides(pptx), Slides(pdf), Matching Logic, K framework, UV'10, BIB

Personal tools
Namespaces

Variants
Actions
Navigation