TY - GEN
T1 - Relational decomposition
AU - Beringer, Lennart
PY - 2011
Y1 - 2011
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=80052150548&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=80052150548&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-22863-6_6
DO - 10.1007/978-3-642-22863-6_6
M3 - Conference contribution
AN - SCOPUS:80052150548
SN - 9783642228629
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 39
EP - 54
BT - Interactive Theorem Proving - Second International Conference, ITP 2011, Proceedings
T2 - 2nd International Conference on Interactive Theorem Proving, ITP 2011
Y2 - 22 August 2011 through 25 August 2011
ER -