Venues / OOPSLA /

OOPSLA 2017

66 papers

A model for reasoning about JavaScript promises · Magnus Madsen, Ondrej Lhoták, Frank Tip
A simple soundness proof for dependent object types · Marianna Rapoport, Ifaz Kabir, Paul He, Ondrej Lhoták
A solver-aided language for test input generation · Talia Ringer, Dan Grossman, Daniel Schwartz-Narbonne, Serdar Tasiran
A verified messaging system · William Mansky, Andrew W. Appel, Aleksey Nogin
A volatile-by-default JVM for server applications · Lun Liu, Todd D. Millstein, Madanlal Musuvathi
Abridging source code · Binhang Yuan, Vijayaraghavan Murali, Christopher M. Jermaine
Alpaca: intermittent execution without checkpoints · Kiwan Maeng, Alexei Colin, Brandon Lucia
An auditing language for preventing correlated failures in the cloud · Ennan Zhai, Ruzica Piskac, Ronghui Gu, Xun Lao, Xi Wang
Automated testing of graphics shader compilers · Alastair F. Donaldson, Hugues Evrard, Andrei Lascu, Paul Thomson
Automatically generating features for learning program analysis heuristics for C-like languages · Kwonsoo Chae, Hakjoo Oh, Kihong Heo, Hongseok Yang
Bounded exhaustive test-input generation on GPUs · Ahmet Çelik, Sreepathi Pai, Sarfraz Khurshid, Milos Gligoric
Data-driven context-sensitivity for points-to analysis · Sehun Jeong, Minseok Jeon, Sung Deok Cha, Hakjoo Oh
Deadlock avoidance in parallel programs with futures: why parallel tasks should not wait for strangers · Tiago Cogumbreiro, Rishi Surendran, Francisco Martins, Vivek Sarkar, Vasco T. Vasconcelos, Max Grossman
Detecting argument selection defects · Andrew Rice, Edward Aftandilian, Ciera Jaspan, Emily Johnston, Michael Pradel, Yulissa Arroyo-Paredes
DéjàVu: a map of code duplicates on GitHub · Cristina V. Lopes, Petr Maj, Pedro Martins, Vaibhav Saini, Di Yang, Jakub Zitny + 2 more
Effective interactive resolution of static analysis alarms · Xin Zhang, Radu Grigore, Xujie Si, Mayur Naik
Efficient logging in non-volatile memory by exploiting coherency protocols · Nachshon Cohen, Michal Friedman, James R. Larus
Evaluating and improving semistructured merge · Guilherme Cavalcanti, Paulo Borba, Paola R. G. Accioly
Exploiting implicit beliefs to resolve sparse usage problem in usage-based specification mining · Syeda Khairunnesa Samantha, Hoan Anh Nguyen, Tien N. Nguyen, Hridesh Rajan
FairSquare: probabilistic verification of program fairness · Aws Albarghouthi, Loris D'Antoni, Samuel Drews, Aditya V. Nori
Familia: unifying interfaces, type classes, and family polymorphism · Yizhou Zhang, Andrew C. Myers
Fast and precise type checking for JavaScript · Avik Chaudhuri, Panagiotis Vekris, Sam Goldman, Marshall Roch, Gabriel Levi
GLORE: generalized loop redundancy elimination upon LER-notation · Yufei Ding, Xipeng Shen
Geo-distribution of actor-based services · Philip A. Bernstein, Sebastian Burckhardt, Sergey Bykov, Natacha Crooks, Jose M. Faleiro, Gabriel Kliot + 5 more
Heaps don't lie: countering unsoundness with heap snapshots · Neville Grech, George Fourtounis, Adrian Francalanza, Yannis Smaragdakis
How type errors were fixed and what students did? · Baijun Wu, Sheng Chen
IDEal: efficient and precise alias-aware dataflow analysis · Johannes Späth, Karim Ali, Eric Bodden
Instrumentation bias for dynamic data race detection · Benjamin P. Wood, Man Cao, Michael D. Bond, Dan Grossman
Learning to blame: localizing novice type errors with data-driven diagnosis · Eric L. Seidel, Huma Sibghat, Kamalika Chaudhuri, Westley Weimer, Ranjit Jhala
Learning user friendly type-error messages · Baijun Wu, John Peter Campora III, Sheng Chen
Model checking copy phases of concurrent copying garbage collection with various memory models · Tomoharu Ugawa, Tatsuya Abe, Toshiyuki Maeda
Model-assisted machine-code synthesis · Venkatesh Srinivasan, Ara Vartanian, Thomas W. Reps
Monadic composition for deterministic, parallel batch processing · Ryan G. Scott, Omar S. Navarro Leija, Joseph Devietti, Ryan R. Newton
Natural synthesis of provably-correct data-structure manipulations · Xiaokang Qiu, Armando Solar-Lezama
Orca: GC and type system co-design for actor languages · Sylvan Clebsch, Juliana Franco, Sophia Drossopoulou, Albert Mingkun Yang, Tobias Wrigstad, Jan Vitek
P/Taint: unified points-to and taint analysis · Neville Grech, Yannis Smaragdakis
Paxos made EPR: decidable reasoning about distributed protocols · Oded Padon, Giuliano Losa, Mooly Sagiv, Sharon Shoham
Practical initialization race detection for JavaScript web applications · Christoffer Quist Adamsen, Anders Møller, Frank Tip
Project snowflake: non-blocking safe manual memory management in .NET · Matthew J. Parkinson, Dimitrios Vytiniotis, Kapil Vaswani, Manuel Costa, Pantazis Deligiannis, Dylan McDermott + 2 more
Reasoning on divergent computations with coaxioms · Davide Ancona, Francesco Dagnino, Elena Zucca
Reliable and automatic composition of language extensions to C: the ableC extensible language framework · Ted Kaminski, Lucas Kramer, Travis Carlson, Eric Van Wyk
Restricting grammars with tree automata · Michael D. Adams, Matthew Might
Robust and compositional verification of object capability patterns · David Swasey, Deepak Garg, Derek Dreyer
SAVI objects: sharing and virtuality incorporated · Izzat El Hajj, Thomas B. Jablin, Dejan S. Milojicic, Wen-Mei W. Hwu
SQLizer: query synthesis from natural language · Navid Yaghmazadeh, Yuepeng Wang, Isil Dillig, Thomas Dillig
Seam: provably safe local edits on graphs · Manolis Papadakis, Gilbert Louis Bernstein, Rahul Sharma, Alex Aiken, Pat Hanrahan
Skip blocks: reusing execution history to accelerate web scripts · Sarah E. Chasins, Rastislav Bodík
Sound gradual typing is nominally alive and well · Fabian Muehlboeck, Ross Tate
Sound gradual typing: only mostly dead · Spenser Bauman, Carl Friedrich Bolz-Tereick, Jeremy G. Siek, Sam Tobin-Hochstadt
Static placement of computation on heterogeneous devices · Gabriel Poesia, Breno Campos Ferreira Guimarães, Fabricio Ferracioli, Fernando Magno Quintão Pereira
Static stages for heterogeneous programming · Adrian Sampson, Kathryn S. McKinley, Todd Mytkowicz
Synthesis of data completion scripts using finite tree automata · Xinyu Wang, Isil Dillig, Rishabh Singh
Synthesizing configuration file specifications with association rule learning · Mark Santolucito, Ennan Zhai, Rahul Dhodapkar, Aaron Shim, Ruzica Piskac
The VM already knew that: leveraging compile-time knowledge to optimize gradual typing · Gregor Richards, Ellen Arteca, Alexi Turcotte
The tensor algebra compiler · Fredrik Kjolstad, Shoaib Kamil, Stephen Chou, David Lugato, Saman P. Amarasinghe
TiML: a functional language for practical complexity analysis with invariants · Peng Wang, Di Wang, Adam Chlipala
Transforming programs and tests in tandem for fault localization · Xia Li, Lingming Zhang
TreeFuser: a framework for analyzing and fusing general recursive tree traversals · Laith Sakka, Kirshanthan Sundararajah, Milind Kulkarni
Type test scripts for TypeScript testing · Erik Krogh Kristensen, Anders Møller
Understanding the use of lambda expressions in Java · Davood Mazinanian, Ameya Ketkar, Nikolaos Tsantalis, Danny Dig
Unifying typing and subtyping · Yanpeng Yang, Bruno C. d. S. Oliveira
Verifying distributed programs via canonical sequentialization · Alexander Bakst, Klaus von Gleissenthall, Rami Gökhan Kici, Ranjit Jhala
Verifying spatial properties of array computations · Dominic A. Orchard, Mistral Contrastin, Matthew Danish, Andrew C. Rice
Verifying strong eventual consistency in distributed systems · Victor B. F. Gomes, Martin Kleppmann, Dominic P. Mulligan, Alastair R. Beresford
Virtual machine warmup blows hot and cold · Edd Barrett, Carl Friedrich Bolz-Tereick, Rebecca Killick, Sarah Mount, Laurence Tratt
Who guards the guards? formal validation of the Arm v8-m architecture specification · Alastair Reid