Matching logic: A new program verification approach (NIER track)

Grigore Roşu, Andrei Ştefǎnescu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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: (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 program execution, 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 subpatterns 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.

Original languageEnglish (US)
Title of host publicationICSE 2011 - 33rd International Conference on Software Engineering, Proceedings of the Conference
Pages868-871
Number of pages4
DOIs
StatePublished - 2011
Event33rd International Conference on Software Engineering, ICSE 2011 - Waikiki, Honolulu, HI, United States
Duration: May 21 2011May 28 2011

Publication series

NameProceedings - International Conference on Software Engineering
ISSN (Print)0270-5257

Other

Other33rd International Conference on Software Engineering, ICSE 2011
Country/TerritoryUnited States
CityWaikiki, Honolulu, HI
Period5/21/115/28/11

Keywords

  • matching logic
  • maude
  • rewriting logic

ASJC Scopus subject areas

  • Software

Fingerprint

Dive into the research topics of 'Matching logic: A new program verification approach (NIER track)'. Together they form a unique fingerprint.

Cite this