Max Planck Institute for Software Systems

4/13/2012

11:00am-12:00pm

The "relational" approach to program verification involves showing that some lower-level program of interest is equivalent to (or a refinement of) some higher-level program, which may in turn prove more amenable to traditional verification techniques. Thanks to recent advances in theorem proving technology, the relational approach has been shown to scale to the verification of significant software systems, such as seL4 and the certified CompCert compiler for C.

However, existing relational methods apply only to the verification of
*whole* software systems. For instance, the correctness of the CompCert
compiler is guaranteed only when it is used to compile whole programs, since
the underlying proof method lacks *compositionality*. Informally,
compositionality means that the verification of a whole program may be obtained
by composing together the verification of its modular subcomponents.

In this talk, I will present two notions of compositionality arising in
relational verification -- horizontal and vertical compositionality --
and discuss the extent to which existing relational techniques do or do not
support them. I will then discuss my own work toward fully compositional
inter-language relational verification, in particular: (1) the development of
a compositional, *semantic* notion of equivalence between high- and
low-level languages, and (2) the invention of a novel relational technique,
*parametric bisimulations*, which supports both horizontal and vertical
notions of compositionally.

**Chung-Kil Hur** is a postdoctoral researcher at
the Max Planck Institute for Software Systems (MPI-SWS). He obtained a PhD from
the University of Cambridge and a BS in Computer Science and in Mathematics
from Korea Advanced Institute of Science and Technology (KAIST). His research
interests are in program verification, interactive theorem proving, semantics,
and category theory.

*Hosted by Jeremy Siek.*

Department of Computer Science

University of Colorado Boulder

Boulder, CO 80309-0430 USA

webmaster@cs.colorado.edu

University of Colorado Boulder

Boulder, CO 80309-0430 USA

webmaster@cs.colorado.edu