Write a Blog >>
DLS 2018
Sun 4 - Fri 9 November 2018 Boston, Massachusetts, United States
co-located with SPLASH 2018

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:

OOPSLA Distinguished Reviewer

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

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:

OOPSLA Distinguished Artifact Evaluation Committee Member

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:

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:

SLE Distinguished reviewer

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

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:

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.