skip to main content
Department of Computer Science University of Colorado Boulder
cu: home | engineering | mycuinfo | about | cu a-z | search cu | contact cu cs: about | calendar | directory | catalog | schedules | mobile | contact cs
home · events · colloquia · 2011-2012 · 

Colloquium - Hur

DLC 1B70

Compositional Inter-Language Relational Verification
Max Planck Institute for Software Systems

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.

The Department holds colloquia throughout the Fall and Spring semesters. These colloquia, open to the public, are typically held on Thursday afternoons, but sometimes occur at other times as well. If you would like to receive email notification of upcoming colloquia, subscribe to our Colloquia Mailing List. If you would like to schedule a colloquium, see Colloquium Scheduling.

Sign language interpreters are available upon request. Please contact Stephanie Morris at least five days prior to the colloquium.

See also:
Department of Computer Science
College of Engineering and Applied Science
University of Colorado Boulder
Boulder, CO 80309-0430 USA
Send email to

Engineering Center Office Tower
ECOT 717
FAX +1-303-492-2844
XHTML 1.0/CSS2 ©2012 Regents of the University of Colorado
Privacy · Legal · Trademarks
May 5, 2012 (13:29)