Sciweavers

Share
PLDI
2009
ACM

Proving optimizations correct using parameterized program equivalence

9 years 5 months ago
Proving optimizations correct using parameterized program equivalence
Translation validation is a technique for checking that, after an optimization has run, the input and output of the optimization are equivalent. Traditionally, translation validation has been used to prove concrete, fully specified programs equivalent. In this paper we present Parameterized Equivalence Checking (PEC), a generalization of translation validation that can prove the equivalence of parameterized programs. A parameterized program is a partially specified program that can represent multiple concrete programs. For example, a parameterized program may contain a section of code whose only known property is that it does not modify certain variables. By proving parameterized programs equivalent, PEC can prove the correctness of transformation rules that represent complex optimizations once and for all, before they are ever run. We implemented our PEC technique in a tool that can establish the equivalence of two parameterized programs. To highlight the power of PEC, we designed ...
Sudipta Kundu, Zachary Tatlock, Sorin Lerner
Added 19 May 2010
Updated 19 May 2010
Type Conference
Year 2009
Where PLDI
Authors Sudipta Kundu, Zachary Tatlock, Sorin Lerner
Comments (0)
books