Ranjit Jhala Receives “Test of Time” Award

Sometimes the best way to judge the importance of work is to view it in hindsight. An idea that might have seemed important or groundbreaking at the time of its publication can prove to be a dead end while another modest proposal that was overlooked when it first came out eventually becomes the way that things are done in its field. With this in mind, many sub-fields in computer science have taken to presenting annual “test of time” awards to work that has proven to be most influential. Every year at the ACM Symposium on Principles of Programming Languages (POPL), the program committee announces the recipient of the POPL Most Influential Paper Award. The committee goes back a decade to the POPL program and determines which of the papers published ten years prior has proven to be of the greatest contemporary value to the field.

In January 2014, the POPL committee recognized the 2004 paper, “Abstractions from Proofs,” co-authored by CNS Professor Ranjit Jhala while he was finishing up his doctoral work at UC Berkeley with his colleagues Tom Henzinger, Rupak Majumdar, and Ken McMillan. The committee explained that in this paper Jhala and his team “demonstrated a fundamental generalization of Craig interpolation to program analysis by predicate abstraction, opening the door for interpolation to be applied to abstraction refinement for ‘infinite-state’ systems.” Prior to the publication of this paper, interpolation had only been used by those researching programming languages in the model checking of “finite-state” systems. The award committee further praised how Jhala’s paper “showed how interpolation offers a fundamental way to explain abstraction refinement in a logical framework, and has led to many extensions to increase the power of abstraction in program analysis.