POPL 2017
Sun 15 - Sat 21 January 2017
Thu 19 Jan 2017 10:30 - 10:55 at Amphitheater 44 - Program Analysis Chair(s): Francesco Logozzo

Establishing quantitative bounds on the execution cost of programs is essential in many areas of computer science such as complexity analysis, compiler optimizations, security and privacy. Techniques based on program analysis, type systems and abstract interpretation are well-studied, but methods for analyzing how the execution costs of two programs compare to each other have not received attention. Naively combining the worst and best case execution costs of the two programs does not work well in many cases because such analysis forgets the similarities between the programs or the inputs.

In this work, we propose a relational cost analysis technique that is capable of establishing precise bounds on the difference in the execution cost of two programs by making use of relational properties of programs and inputs. We develop RelCost, a refinement type and effect system for a higher-order functional language with recursion and subtyping. The key novelty of our technique is the combination of relational refinements with two modes of typing—relational typing for reasoning about similar computations/inputs and standard typing for reasoning about unrelated computations/inputs. This combination allows us to analyze execution cost difference of programs more precisely than a naive non-relational approach.

We prove our type system sound using a novel semantic model based on step-indexed unary and binary logical relations accounting for non-relational and relational reasoning principles with their respective costs. We demonstrate the precision and generality of our technique through examples.

Thu 19 Jan
Times are displayed in time zone: (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

10:30 - 12:10: POPL - Program Analysis at Amphitheater 44
Chair(s): Francesco LogozzoFacebook
POPL-2017-papers10:30 - 10:55
Ezgi ÇiçekMPI-SWS, Germany, Gilles BartheIMDEA, Marco GaboardiSUNY Buffalo, USA, Deepak GargMPI-SWS, Germany, Jan HoffmannCarnegie Mellon University
POPL-2017-papers10:55 - 11:20
Ravichandhran MadhavanEPFL, Sumith KulalIIT Bombay, Viktor KunčakEPFL, Switzerland
POPL-2017-papers11:20 - 11:45
Qirun ZhangUniversity of California, Davis, Zhendong SuUniversity of California, Davis
POPL-2017-papers11:45 - 12:10
Jan HoffmannCarnegie Mellon University, Ankush DasCarnegie Mellon University, Shu-chun WengYale University