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.

OOPSLA Distinguished Paper

The following papers were selected by the OOPSLA committee and external committee for distinguished paper awards:

• MadMax: Surviving Out-of-Gas Conditions in Ethereum Smart Contracts, Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, Yannis Smaragdakis
• BioScript: programming safe chemistry on laboratories-on-a-chip, Jason Ott, Tyson Loveless, Chris Curtis, Mohsen Lesani, Philip Brisk
• Gradual Liquid Type Inference, Niki Vazou, Éric Tanter, David Van Horn
• Randomized Testing of Distributed Systems with Probabilistic Guarantees, Burcu Kulahcioglu Ozkan, Rupak Majumdar, Filip Niksic, Mitra Tabaei Befrouei, Georg Weissenbacher

OOPSLA Distinguished Reviewer

The following reviewers were selected by the OOPSLA chair for distinguished reviewer awards:

• Colin Gordon, Drexel University, USA
• Derek Dreyer, MPI-SWS, Germany

Student Research Competition

For more information, please see the SRC Awards page.

The competition winners were, in each category:

Graduate Category

• Matthias Springer for SoaAlloc: Accelerating Single-Method Multiple-Objects Applications on GPUs
• Kirshanthan Sundararajah for Scheduling Transformations and Dependence Tests for Recursive Programs

Undergraduate Category

• Justin Lubin for Approximating Polymorphic Effects with Capabilities
• Paulette Koronkevich for Obsidian in the Rough: A Case Study Evaluation of a New Blockchain Programming Language
• Serena Chen for Finding Higher Order Mutants Using Variational Execution

OOPSLA Distinguished Artifact

The following artifacts were selected to receive Distinguished Artifact Awards by the OOPSLA artifact evaluation committee:

• 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 Research Paper

The following paper was selected by the SLE program committee chairs based on the recommendations of the program committee for distinguished paper research award:

• Facet-Oriented Modelling: Open Objects for Model-Driven Engineering, Juan de Lara, Esther Guerra, Jörg Kienzle, Yanis Hattab

SLE Distinguished Vision Paper

The following paper was selected by the SLE program committee chairs based on the recommendations of the program committee for distinguished paper vision award:

• Shape-Diverse DSLs: Languages without Borders, Fabien Coulon, Thomas Degueule, Tijs van der Storm, Benoit Combemale

SLE Distinguished reviewer

The following reviewer was selected by the SLE program committee chairs for distinguished reviewer award:

• Erwan Bousse, TU Wien, Austria

SLE Distinguished artifact

The following artifact was selected by the SLE artifact evaluation chairs based on the recommendations of the artifact evaluation committee for distinguished artifact award:

• Modular Language Composition for the Masses, Manuel Leduc, Thomas Degueule, Benoit Combemale

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.