Matching Logic

From FSL

Matching logic is an alternative to Hoare logics in which the state structure plays a crucial role. Program states are represented as algebraic datatypes called (concrete) configurations, and program state specifications are represented as configuration terms with variables and constraints on them called (configuration) patterns. A pattern specifies those configurations that match it. Patterns can bind variables to their scope, allowing both for pattern abstraction and for expressing loop invariants.

[edit] Theory

• July 2009 From Rewriting Logic Executable Semantics to Matching Logic Program Verification: This report frames ML within FOL₌ and shows how to derive ML verifiers from K definitions of languages.
• January 2009 Matching Logic --- Extended Report: This report defines ML as an alternative (to Hoare logic) axiomatic semantic framework.

[edit] Implementation

• Download first prototype (Implemented in Maude)
  • This version comes with the Schorr-Waite algorithm as well as programs using lists, queues, and trees.
• Download latest prototype (Implemented in K-Maude)
  • This version is a complete rewrite using our new K-Maude tool. The zip contains over 100 example programs written in HIMP including many typical Hoare-level programs (sum to n, fibonacci, factorial) as well as some linked list programs (append, reverse, and length).
• Download language pack
  • This includes executable definitions of the IMP, HIMP, and KernelC languages written in K-Maude, together with example programs for each.