Skip to main content

Matching Logic - An Alternative to Hoare/Floyd/Separation Logics for Program Verification

Grigore Rosu ( University of Illinois at Urbana-Champaign )

Matching logic is a novel framework for defining axiomatic semantics
to programming languages.  Matching logic specifications are
particular first-order formulae with constrained algebraic structure,
called *patterns*.  Program configurations satisfy patterns iff they
*match* their algebraic structure and satisfy their constraints.
This direct structural relationship between concrete program
configurations and matching logic program specifications allows for
the natural development of forwards-analysis program verifiers that do
not introduce quantifiers, resembling operational semantics.

Extending a language with a heap and operations on it, while easy to
define using operational semantics, is a non-trivial task for Hoare
logic, often requiring to extend its underlying logical formalism to
separation or other non-first-order logics.  We show that extending
a simple language with a heap, dynamic memory allocation and pointer
arithmetic, is as easy and natural in matching logic as it is in
operational semantics, requiring no extension of the underlying
first-order logic; moreover, heap patterns such as lists, trees,
queues, graphs, etc., can be defined algebraically using fist-order
constraints over patterns.

An efficient matching logic program verifier implemented in Maude will
be also briefly discussed and, if time permits, demoed.  This verifier
is directly derived from an executable rewrite logic semantics of the
programming language.

Speaker Bio:

Grigore Rosu is an associate professor in the Department of Computer
Science at the University of Illinois at Urbana-Champaign (UIUC),
where he leads the Formal Systems Laboratory (FSL).  His research
interests encompass both theoretical foundations and system
development in the areas of formal methods, software engineering and
programming languages.  Before joining UIUC in 2002, he was a research
scientist at NASA Ames.  He obtained his Ph.D. at the University of
California at San Diego in 2000 and his M.S. at the University of
Bucharest, Romania, in 1996. He was offered the CAREER award by the
NSF and the outstanding junior award by the Computer Science
Department at UIUC in 2005.  He won an ACM SIGSOFT distinguished paper
award at ASE 2008 and the best software science paper award at ETAPS
2002.  He was ranked a UIUC excellent teacher in Spring 2008 and Fall

Share this: