[Pl-seminar] 11/16: Grigore Rosu, "K and Matching Logic"

[Christos Dimoulas]

NEU Programming Languages Seminar presents

Grigore Rosu
Formal Systems Laboratory (FSL)
Department of Computer Science
University of Illinois at Urbana-Champaign

Wednesday, 11/16

11:45am - 1:30pm
Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)


Title: K and Matching Logic

Abstract:: Would you like to wake up some morning, have a coffee, then 
design a non-trivial programming language, say with multidimensional 
arrays and array references, with functions and references to them, with 
blocks and local declarations, with input/output, with exceptions, with 
nondeterminism and concurrency with synchronization, and so on, and by 
evening to have a reasonably efficient interpreter, a state-space search 
tool and a model checker, as well as a deductive program verifier for 
your language, all correct-by-construction? Then you may be interested 
in K and Matching Logic, because that is what they are aiming for. K is 
a rewrite-based framework for defining formal operational semantics of 
programming languages. A K semantics can be executed, and thus tested, 
as if it was an interpreter for the defined language. This way, we can 
gain confidence in the correctness of our semantics. Then we can use 
precisely that semantics, unchanged, for program analysis and 
verification, without a need to give the language another, e.g., 
axiomatic or denotational or dynamic, semantics. Matching logic consists 
of a language-independent proof system that allows us to reason about 
programs in any language that is given a rewrite-based operational 
semantics.

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 2004.