Relational decomposition

Lennart Beringer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

20 Scopus citations


We introduce relational decomposition, a technique for formally reducing termination-insensitive relational program logics to unary logics, that is program logics for one-execution properties. Generalizing the approach of self-composition, we develop a notion of interpolants that decompose along the phrase structure, and relate these interpolants to unary and relational predicate transformers. In contrast to previous formalisms, relational decomposition is applicable across heterogeneous pairs of transition systems. We apply our approach to justify variants of Benton's Relational Hoare Logic (RHL) for a language with objects, and present novel rules for relating loops that fail to proceed in lockstep. We also outline applications to noninterference and separation logic.

Original languageEnglish (US)
Title of host publicationInteractive Theorem Proving - Second International Conference, ITP 2011, Proceedings
Number of pages16
StatePublished - 2011
Externally publishedYes
Event2nd International Conference on Interactive Theorem Proving, ITP 2011 - Berg en Dal, Netherlands
Duration: Aug 22 2011Aug 25 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume6898 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349


Conference2nd International Conference on Interactive Theorem Proving, ITP 2011
CityBerg en Dal

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


Dive into the research topics of 'Relational decomposition'. Together they form a unique fingerprint.

Cite this