Awards

SIGPLAN Most Influential OOPSLA Paper Award

• Dino Distefano, Facebook and Queen Mary University of London, and Matthew J. Parkinson, Microsoft Research for jStar: towards practical verification for java: The jStar paper is notable for introducing an approach to specifying OO design patterns that has since become standard and is used in modern tools such as VeriFast. The approach is amenable to automation and extends to patterns such as Subject-Observer, in which there is not a strict hierarchical relationship between objects. The paper also describes a fully automated verification approach that required no proof hints within methods, inspiring the development of a number of later verification tools for separation logic.

OOSPLA Distinguished Paper

• Announced at the conference.

OOPSLA Distinguished Reviewer

• Announced at the conference.

Student Research Competition

• Announced at the conference.

OOPSLA Distinguished Artifact

• James Bornholt and Emina Torlak, University of Washington, for Finding Code That Explodes Under Symbolic Evaluation
• Remigius Meier ETHZ, Armin Rigo PyPy, Thomas Gross ETHZ, for Virtual Machine Design for Parallel Dynamic Programming Languages

OOPSLA Distinguished Artifact Evaluation Committee Member

• Molly Feldman, Cornell
• Juliana Franco, Microsoft Research
• Sungho Lee, KAIST

SLE Distinguished paper

• Award for most notable paper, as determined by the PC chairs based on the recommendations of the programme committee.

SLE Distinguished reviewer

• Award for distinguished reviewer, as determined by the PC chairs.

SLE Distinguished artifact

• Award for the artifact most significantly exceeding expectations, as determined by the AEC chairs based on the recommendations of the artifact evaluation committee.

SIGPLAN John C. Reynolds Doctoral Dissertation Award

• David Menendez, Rutgers University for Practical Formal Techniques and Tools for Developing LLVM’s Peephole Optimizations: This thesis proposes abstractions and formal tools to develop correct LLVM peephole optimizations. A domain specific language (DSL) Alive enables the specification and verification of peephole optimizations. An Alive transformation is shown to be correct automatically by encoding the transformation and correctness criteria as constraints in first-order logic, which are automatically checked for validity using an SMT solver. It then generates C++ code for an LLVM pass. Peephole optimizations in LLVM are executed numerous times until no optimization is applicable and one optimization could undo the effect of the other resulting in non-terminating compilation. A novel algorithm based on directed-acyclic-graph (DAG) composition determines whether such non-termination bugs can occur with a suite of peephole optimizations. The Alive toolkit can generate concrete input to demonstrate non-termination as well as automatically generating weakest preconditions. It is actively used by the LLVM community and has detected numerous bugs in existing passes and is preventing bugs from being added to the compiler.