OOPSLA 2020
Proceedings of the ACM on Programming Languages, Volume 4, Number OOPSLA

Title Page

Article: oopsla20foreword-fm000-p doi:

Editorial Message

Article: oopsla20foreword-fm001-p doi:

Fixpoints for the Masses: Programming with First-Class Datalog Constraints
Magnus Madsen and Ondřej Lhoták
(Aarhus University, Denmark; University of Waterloo, Canada)

Publisher's Version Video Article: oopsla20main-p5-p doi:10.1145/3428193

Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
Jonathan Immanuel Brachthäuser, Philipp Schuster, and Klaus Ostermann
(EPFL, Switzerland; University of Tübingen, Germany)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p6-p doi:10.1145/3428194

A Systematic Approach to Deriving Incremental Type Checkers
André Pacak, Sebastian Erdweg, and Tamás Szabó
(University of Mainz, Germany; itemis, Germany)

Publisher's Version Video Article: oopsla20main-p11-p doi:10.1145/3428195

Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, and Sharon Shoham
(Tel Aviv University, Israel; University of Paris Diderot, France; IMDEA Software Institute, Spain)

Publisher's Version Video Article: oopsla20main-p13-p doi:10.1145/3428196

Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
Cyril Six, Sylvain Boulmé, and David Monniaux
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p14-p doi:10.1145/3428197

Enabling Accuracy-Aware Quantum Compilers using Symbolic Resource Estimation
Giulia Meuli, Mathias Soeken, Martin Roetteler, and Thomas Häner
(EPFL, Switzerland; Microsoft, Switzerland; Microsoft, USA)

Publisher's Version Video Article: oopsla20main-p19-p doi:10.1145/3428198

Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
Guilherme Vieira Leobas and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil)

Publisher's Version Video Article: oopsla20main-p22-p doi:10.1145/3428199

Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
Michael Coblenz, Jonathan Aldrich, Brad A. Myers, and Joshua Sunshine
(Carnegie Mellon University, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p23-p doi:10.1145/3428200

Assertion-Based Optimization of Quantum Programs
Thomas Häner, Torsten Hoefler, and Matthias Troyer
(ETH Zurich, Switzerland; Microsoft, USA)

Publisher's Version Video Article: oopsla20main-p24-p doi:10.1145/3428201

Multiparty Motion Coordination: From Choreographies to Robotics Programs
Rupak Majumdar, Nobuko Yoshida, and Damien Zufferey
(MPI-SWS, Germany; Imperial College London, UK)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p25-p doi:10.1145/3428202

Automated Policy Synthesis for System Call Sandboxing
Shankara Pailoor, Xinyu Wang, Hovav Shacham, and Isil Dillig
(University of Texas at Austin, USA; University of Michigan, USA)

Publisher's Version Video Article: oopsla20main-p28-p doi:10.1145/3428203

How Do Programmers Use Unsafe Rust?
Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller, and Alexander J. Summers
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Publisher's Version Video Article: oopsla20main-p32-p doi:10.1145/3428204

Learning Semantic Program Embeddings with Graph Interval Neural Network
Yu Wang, Ke Wang, Fengjuan Gao, and Linzhang Wang
(Nanjing University, China; Visa Research, USA)

Publisher's Version Video Article: oopsla20main-p37-p doi:10.1145/3428205

Mossad: Defeating Software Plagiarism Detection
Breanna Devore-McDonald and Emery D. Berger
(University of Massachusetts at Amherst, USA)

Publisher's Version Video Article: oopsla20main-p40-p doi:10.1145/3428206

Handling Bidirectional Control Flow
Yizhou Zhang, Guido Salvaneschi, and Andrew C. Myers
(University of Waterloo, Canada; University of St. Gallen, Switzerland; Cornell University, USA)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p51-p doi:10.1145/3428207

Scaling Exact Inference for Discrete Probabilistic Programs
Steven Holtzen, Guy Van den Broeck, and Todd Millstein
(University of California at Los Angeles, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p56-p doi:10.1145/3428208

Formulog: Datalog for SMT-Based Static Analysis
Aaron Bembenek, Michael Greenberg, and Stephen Chong
(Harvard University, USA; Pomona College, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p65-p doi:10.1145/3428209

Precise Inference of Expressive Units of Measurement Types
Tongtong Xiang, Jeff Y. Luo, and Werner Dietl
(University of Waterloo, Canada)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p67-p doi:10.1145/3428210

WATCHER: In-Situ Failure Diagnosis
Hongyu Liu, Sam Silvestro, Xiangyu Zhang, Jian Huang, and Tongping Liu
(Purdue University, USA; University of Texas at San Antonio, USA; University of Illinois at Urbana-Champaign, USA; University of Massachusetts at Amherst, USA)

Publisher's Version Video Article: oopsla20main-p70-p doi:10.1145/3428211

A Model for Detecting Faults in Build Specifications
Thodoris Sotiropoulos, Stefanos Chaliasos, Dimitris Mitropoulos, and Diomidis Spinellis
(Athens University of Economics and Business, Greece)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p78-p doi:10.1145/3428212

Guided Linking: Dynamic Linking without the Costs
Sean Bartell, Will Dietz, and Vikram S. Adve
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p80-p doi:10.1145/3428213

Satune: Synthesizing Efficient SAT Encoders
Hamed Gorjiara, Guoqing Harry Xu, and Brian Demsky
(University of California at Irvine, USA; University of California at Los Angeles, USA)

Publisher's Version Video Article: oopsla20main-p82-p doi:10.1145/3428214

Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
Shengjian Guo, Yueqi Chen, Jiyong Yu, Meng Wu, Zhiqiang Zuo, Peng Li, Yueqiang Cheng, and Huibo Wang
(Baidu Security, USA; Pennsylvania State University, USA; University of Illinois at Urbana-Champaign, USA; Ant Group, China; Nanjing University, China)

Publisher's Version Video Article: oopsla20main-p84-p doi:10.1145/3428215

Statically Verified Refinements for Multiparty Protocols
Fangyi Zhou, Francisco Ferreira, Raymond Hu, Rumyana Neykova, and Nobuko Yoshida
(Imperial College London, UK; University of Hertfordshire, UK; Brunel University London, UK)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p87-p doi:10.1145/3428216

Featherweight Go
Robert Griesemer, Raymond Hu, Wen Kokke, Julien Lange, Ian Lance Taylor, Bernardo Toninho, Philip Wadler, and Nobuko Yoshida
(Google, USA; University of Hertfordshire, UK; University of Edinburgh, UK; Royal Holloway University of London, UK; Nova University of Lisbon, Portugal; NOVA-LINCS, Portugal; Imperial College London, UK)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p91-p doi:10.1145/3428217

Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs
Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, and Yuan Xie
(University of California at Santa Barbara, USA; MPI-SP, Germany; University of Technology Sydney, Australia; Institute of Software at Chinese Academy of Sciences, China; Tsinghua University, China)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p92-p doi:10.1145/3428218

Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-x86
Azalea Raad, Ori Lahav, and Viktor Vafeiadis
(MPI-SWS, Germany; Imperial College London, UK; Tel Aviv University, Israel)

Publisher's Version Video Article: oopsla20main-p93-p doi:10.1145/3428219

Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Christoph Sprenger, Tobias Klenze, Marco Eilers, Felix A. Wolf, Peter Müller, Martin Clochard, and David Basin
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p95-p doi:10.1145/3428220

DiffStream: Differential Output Testing for Stream Processing Programs
Konstantinos Kallas, Filip Niksic, Caleb Stanford, and Rajeev Alur
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p96-p doi:10.1145/3428221

Polymorphic Types and Effects with Boolean Unification
Magnus Madsen and Jaco van de Pol
(Aarhus University, Denmark)

Publisher's Version Video Article: oopsla20main-p97-p doi:10.1145/3428222

CAMP: Cost-Aware Multiparty Session Protocols
David Castro-Perez and Nobuko Yoshida
(Imperial College London, UK)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p100-p doi:10.1145/3428223

The Anchor Verifier for Blocking and Non-blocking Concurrent Software
Cormac Flanagan and Stephen N. Freund
(University of California at Santa Cruz, USA; Williams College, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p103-p doi:10.1145/3428224

Automatic and Efficient Variability-Aware Lifting of Functional Programs
Ramy Shahin and Marsha Chechik
(University of Toronto, Canada)

Publisher's Version Video Article: oopsla20main-p113-p doi:10.1145/3428225

A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra
Ryan Senanayake, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen Chou, Shoaib Kamil, Saman Amarasinghe, and Fredrik Kjolstad
(Reservoir Labs, USA; Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe Research, USA)

Publisher's Version Video Article: oopsla20main-p119-p doi:10.1145/3428226

Programming with a Read-Eval-Synth Loop
Hila Peleg, Roi Gabay, Shachar Itzhaky, and Eran Yahav
(University of California at San Diego, USA; Technion, Israel; Codota, Israel)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p125-p doi:10.1145/3428227

LiveDroid: Identifying and Preserving Mobile App State in Volatile Runtime Environments
Umar Farooq, Zhijia Zhao, Manu Sridharan, and Iulian Neamtiu
(University of California at Riverside, USA; New Jersey Institute of Technology, USA)

Publisher's Version Video Article: oopsla20main-p129-p doi:10.1145/3428228

Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
Xiaohong Chen, Minh-Thai Trinh, Nishant Rodrigues, Lucas Peña, and Grigore Roşu
(University of Illinois at Urbana-Champaign, USA; Advanced Digital Sciences Center, Singapore)

Publisher's Version Video Article: oopsla20main-p136-p doi:10.1145/3428229

Adversarial Examples for Models of Code
Noam Yefet, Uri Alon, and Eran Yahav
(Technion, Israel)

Publisher's Version Video Article: oopsla20main-p137-p doi:10.1145/3428230

Towards a Formal Foundation of Intermittent Computing
Milijana Surbatovich, Brandon Lucia, and Limin Jia
(Carnegie Mellon University, USA)

Publisher's Version Video Article: oopsla20main-p140-p doi:10.1145/3428231

Compiling Symbolic Execution with Staging and Algebraic Effects
Guannan Wei, Oliver Bračevac, Shangyin Tan, and Tiark Rompf
(Purdue University, USA)

Publisher's Version Video Article: oopsla20main-p141-p doi:10.1145/3428232

Testing Differential Privacy with Dual Interpreters
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce, and Aaron Roth
(University of Pennsylvania, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p143-p doi:10.1145/3428233

Verifying and Improving Halide’s Term Rewriting System with Program Synthesis
Julie L. Newcomb, Andrew Adams, Steven Johnson, Rastislav Bodik, and Shoaib Kamil
(University of Washington, USA; Adobe Research, USA; Google, USA)

Publisher's Version Video Article: oopsla20main-p148-p doi:10.1145/3428234

Dynamic Dispatch of Context-Sensitive Optimizations
Gabriel Poesia and Fernando Magno Quintão Pereira
(Stanford University, USA; Federal University of Minas Gerais, Brazil)

Publisher's Version Video Article: oopsla20main-p149-p doi:10.1145/3428235

Eliminating Abstraction Overhead of Java Stream Pipelines using Ahead-of-Time Program Optimization
Anders Møller and Oskar Haarklou Veileborg
(Aarhus University, Denmark)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p155-p doi:10.1145/3428236

Build Scripts with Perfect Dependencies
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt
(Indiana University, USA; Facebook, UK)

Publisher's Version Video Article: oopsla20main-p169-p doi:10.1145/3428237

Deductive Optimization of Relational Data Storage
John Feser, Sam Madden, Nan Tang, and Armando Solar-Lezama
(Massachusetts Institute of Technology, USA; QCRI HBKU, Qatar)

Publisher's Version Video Article: oopsla20main-p171-p doi:10.1145/3428238

Program Equivalence for Assisted Grading of Functional Programs
Joshua Clune, Vijay Ramamurthy, Ruben Martins, and Umut A. Acar
(Carnegie Mellon University, USA)

Publisher's Version Video Article: oopsla20main-p188-p doi:10.1145/3428239

A Modular Cost Analysis for Probabilistic Programs
Martin Avanzini, Georg Moser, and Michael Schaper
(Inria, France; University of Innsbruck, Austria)

Publisher's Version Video Article: oopsla20main-p190-p doi:10.1145/3428240

Geometry Types for Graphics Programming
Dietrich Geisler, Irene Yoon, Aditi Kabra, Horace He, Yinnon Sanders, and Adrian Sampson
(Cornell University, USA; University of Pennsylvania, USA; Carnegie Mellon University, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p193-p doi:10.1145/3428241

Hidden Inheritance: An Inline Caching Design for TypeScript Performance
Zhefeng Wu, Zhe Sun, Kai Gong, Lingyun Chen, Bin Liao, and Yihua Jin
(Alibaba Group, China)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p194-p doi:10.1145/3428242

A Type-and-Effect System for Object Initialization
Fengyun Liu, Ondřej Lhoták, Aggelos Biboudis, Paolo G. Giarrusso, and Martin Odersky
(EPFL, Switzerland; University of Waterloo, Canada; Delft University of Technology, Netherlands)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p195-p doi:10.1145/3428243

Sound Garbage Collection for C using Pointer Provenance
Subarno Banerjee, David Devecsery, Peter M. Chen, and Satish Narayanasamy
(University of Michigan, USA; Georgia Institute of Technology, USA)

Publisher's Version Video Article: oopsla20main-p196-p doi:10.1145/3428244

Dataflow-Based Pruning for Speeding up Superoptimization
Manasij Mukherjee, Pranav Kant, Zhengyang Liu, and John Regehr
(University of Utah, USA)

Publisher's Version Video Article: oopsla20main-p201-p doi:10.1145/3428245

FlowCFL: Generalized Type-Based Reachability Analysis: Graph Reduction and Equivalence of CFL-Based and Type-Based Reachability
Ana Milanova
(Rensselaer Polytechnic Institute, USA)

Publisher's Version Video Article: oopsla20main-p203-p doi:10.1145/3428246

Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features
Minseok Jeon, Myungho Lee, and Hakjoo Oh
(Korea University, South Korea)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p218-p doi:10.1145/3428247

Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications
Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, and Eelco Visser
(Delft University of Technology, Netherlands)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p222-p doi:10.1145/3428248

Designing Types for R, Empirically
Alexi Turcotte, Aviral Goel, Filip Křikava, and Jan Vitek
(Northeastern University, USA; Czech Technical University, Czechia)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p225-p doi:10.1145/3428249

Shiftry: RNN Inference in 2KB of RAM
Aayan Kumar, Vivek Seshadri, and Rahul Sharma
(Microsoft Research, India)

Publisher's Version Video Article: oopsla20main-p230-p doi:10.1145/3428250

StreamQL: A Query Language for Processing Streaming Time Series
Lingkun Kong and Konstantinos Mamouras
(Rice University, USA)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p232-p doi:10.1145/3428251

Incremental Predicate Analysis for Regression Verification
Qianshan Yu, Fei He, and Bow-Yaw Wang
(Tsinghua University, China; Academia Sinica, Taiwan)

Publisher's Version Video Article: oopsla20main-p233-p doi:10.1145/3428252

Perfectly Parallel Fairness Certification of Neural Networks
Caterina Urban, Maria Christakis, Valentin Wüstholz, and Fuyuan Zhang
(Inria, France; ENS, France; CNRS, France; PSL University, France; MPI-SWS, Germany; ConsenSys, Germany)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p242-p doi:10.1145/3428253

Fuzzing Channel-Based Concurrency Runtimes using Types and Effects
Quentin Stiévenart and Magnus Madsen
(Vrije Universiteit Brussel, Belgium; Aarhus University, Denmark)

Publisher's Version Video Article: oopsla20main-p244-p doi:10.1145/3428254

Detecting Locations in JavaScript Programs Affected by Breaking Library Changes
Anders Møller, Benjamin Barslev Nielsen, and Martin Toldam Torp
(Aarhus University, Denmark)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p245-p doi:10.1145/3428255

Rethinking Safe Consistency in Distributed Object-Oriented Programming
Mirko Köhler, Nafise Eskandani, Pascal Weisenburger, Alessandro Margara, and Guido Salvaneschi
(TU Darmstadt, Germany; Politecnico di Milano, Italy; University of St. Gallen, Switzerland)

Publisher's Version Video Article: oopsla20main-p249-p doi:10.1145/3428256

DynamiTe: Dynamic Termination and Non-termination Proofs
Ton Chanh Le, Timos Antonopoulos, Parisa Fathololumi, Eric Koskinen, and ThanhVu Nguyen
(Stevens Institute of Technology, USA; Yale University, USA; University of Nebraska-Lincoln, USA)

Publisher's Version Video Article: oopsla20main-p256-p doi:10.1145/3428257

Precise Static Modeling of Ethereum “Memory”
Sifis Lagouvardos, Neville Grech, Ilias Tsatiris, and Yannis Smaragdakis
(University of Athens, Greece)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p262-p doi:10.1145/3428258

Taming Type Annotations in Gradual Typing
John Peter Campora and Sheng Chen
(University of Louisiana at Lafayette, USA)

Publisher's Version Video Article: oopsla20main-p271-p doi:10.1145/3428259

Inter-theory Dependency Analysis for SMT String Solvers
Minh-Thai Trinh, Duc-Hiep Chu, and Joxan Jaffar
(Advanced Digital Sciences Center, Singapore; National University of Singapore, Singapore)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p272-p doi:10.1145/3428260

On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
Dominik Winterer, Chengyu Zhang, and Zhendong Su
(ETH Zurich, Switzerland; East China Normal University, China)

Publisher's Version Video Article: oopsla20main-p273-p doi:10.1145/3428261

Pomsets with Preconditions: A Simple Model of Relaxed Memory
Radha Jagadeesan, Alan Jeffrey, and James Riely
(DePaul University, USA; Mozilla Research, USA)

Publisher's Version Video Article: oopsla20main-p286-p doi:10.1145/3428262

Fast Linear Programming through Transprecision Computing on Small and Sparse Data
Tobias Grosser, Theodoros Theodoridis, Maximilian Falkenstein, Arjun Pitchanathan, Michael Kruse, Manuel Rigger, Zhendong Su, and Torsten Hoefler
(University of Edinburgh, UK; ETH Zurich, Switzerland; IIIT Hyderabad, India; Argonne National Laboratory, USA)

Publisher's Version Video Article: oopsla20main-p287-p doi:10.1145/3428263

Random Testing for C and C++ Compilers with YARPGen
Vsevolod Livinskii, Dmitry Babokin, and John Regehr
(University of Utah, USA; Intel Corporation, USA)

Publisher's Version Video Article: oopsla20main-p292-p doi:10.1145/3428264

CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
Yuting Wang, Xiangzhe Xu, Pierre Wilke, and Zhong Shao
(Shanghai Jiao Tong University, China; Nanjing University, China; CentraleSupélec, France; Yale University, USA)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p295-p doi:10.1145/3428265

Scalable and Serializable Networked Multi-actor Programming
Bo Sang, Patrick Eugster, Gustavo Petri, Srivatsan Ravi, and Pierre-Louis Roman
(Purdue University, USA; Ant Group, USA; USI Lugano, Switzerland; TU Darmstadt, Germany; ARM Research, UK; University of Southern California, USA)

Publisher's Version Video Article: oopsla20main-p299-p doi:10.1145/3428266

Termination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules
Fei He and Jitao Han
(Tsinghua University, China)

Publisher's Version Video Article: oopsla20main-p300-p doi:10.1145/3428267

Programming and Reasoning with Partial Observability
Eric Atkinson and Michael Carbin
(Massachusetts Institute of Technology, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p304-p doi:10.1145/3428268

Interactive Synthesis of Temporal Specifications from Examples and Natural Language
Ivan Gavran, Eva Darulova, and Rupak Majumdar
(MPI-SWS, Germany)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p311-p doi:10.1145/3428269

A Large-Scale Longitudinal Study of Flaky Tests
Wing Lam, Stefan Winter, Anjiang Wei, Tao Xie, Darko Marinov, and Jonathan Bell
(University of Illinois at Urbana-Champaign, USA; TU Darmstadt, Germany; Peking University, China; Northeastern University, USA)

Publisher's Version Video Article: oopsla20main-p314-p doi:10.1145/3428270

Differentially-Private Software Frequency Profiling under Linear Constraints
Hailong Zhang, Yu Hao, Sufian Latif, Raef Bassily, and Atanas Rountev
(Fordham University, USA; Ohio State University, USA)

Publisher's Version Video Article: oopsla20main-p334-p doi:10.1145/3428271

Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees Syeda, Magnus O. Myreen, and Yong Kiam Tan
(Chalmers University of Technology, Sweden; Data61 at CSIRO, Australia; UNSW, Australia; Carnegie Mellon University, USA)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p340-p doi:10.1145/3428272

Digging for Fold: Synthesis-Aided API Discovery for Haskell
Michael B. James, Zheng Guo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit Jhala, and Nadia Polikarpova
(University of California at San Diego, USA)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p342-p doi:10.1145/3428273

Resolution as Intersection Subtyping via Modus Ponens
Koar Marntirosian, Tom Schrijvers, Bruno C. d. S. Oliveira, and Georgios Karachalias
(KU Leuven, Belgium; University of Hong Kong, China; Tweag, France)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p345-p doi:10.1145/3428274

World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
Julia Belyakova, Benjamin Chung, Jack Gelinas, Jameson Nash, Ross Tate, and Jan Vitek
(Northeastern University, USA; Julia Computing, USA; Cornell University, USA; Czech Technical University, Czechia)

Publisher's Version Video Article: oopsla20main-p384-p doi:10.1145/3428275

ιDOT: A DOT Calculus with Object Initialization
Ifaz Kabir, Yufeng Li, and Ondřej Lhoták
(University of Alberta, Canada; University of Waterloo, Canada)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p386-p doi:10.1145/3428276

Taming Callbacks for Smart Contract Modularity
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez, Albert Rubio, and Mooly Sagiv
(Complutense University of Madrid, Spain; Tel Aviv University, Israel)

Publisher's Version Video Article: oopsla20main-p401-p doi:10.1145/3428277

Testing Consensus Implementations using Communication Closure
Cezara Drăgoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Filip Niksic
(Inria, France; Informal Systems, France; University of Paris, France; IRIF, France; CNRS, France; MPI-SWS, Germany; University of Pennsylvania, USA)

Publisher's Version Video Article: oopsla20main-p411-p doi:10.1145/3428278

Finding Bugs in Database Systems via Query Partitioning
Manuel Rigger and Zhendong Su
(ETH Zurich, Switzerland)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p413-p doi:10.1145/3428279

Structure Interpretation of Text Formats
Sumit Gulwani, Vu Le, Arjun Radhakrishna, Ivan Radiček, and Mohammad Raza
(Microsoft, USA; Microsoft, Austria)

Publisher's Version Video Article: oopsla20main-p421-p doi:10.1145/3428280

Programming at the Edge of Synchrony
Cezara Drăgoi, Josef Widder, and Damien Zufferey
(Inria, France; ENS, France; CNRS, France; PSL University, France; Informal Systems, France; Informal Systems, Austria; MPI-SWS, Germany)

Publisher's Version Article: oopsla20main-p424-p doi:10.1145/3428281

Actor Concurrency Bugs: A Comprehensive Study on Symptoms, Root Causes, API Usages, and Differences
Mehdi Bagherzadeh, Nicholas Fireman, Anas Shawesh, and Raffi Khatchadourian
(Oakland University, USA; City University of New York, USA)

Publisher's Version Video Article: oopsla20main-p451-p doi:10.1145/3428282

A Structural Model for Contextual Code Changes
Shaked Brody, Uri Alon, and Eran Yahav
(Technion, Israel)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p467-p doi:10.1145/3428283

Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
Yiyun Liu, James Parker, Patrick Redmond, Lindsey Kuper, Michael Hicks, and Niki Vazou
(University of Maryland at College Park, USA; University of California at Santa Cruz, USA; IMDEA Software Institute, Spain)

Publisher's Version Video Artifacts Functional Article: oopsla20main-p469-p doi:10.1145/3428284

Unifying Execution of Imperative Generators and Declarative Specifications
Pengyu Nie, Marinela Parovic, Zhiqiang Zang, Sarfraz Khurshid, Aleksandar Milicevic, and Milos Gligoric
(University of Texas at Austin, USA; Microsoft, USA)

Publisher's Version Video Article: oopsla20main-p473-p doi:10.1145/3428285

Regex Matching with Counting-Set Automata
Lenka Turoňová, Lukáš Holík, Ondřej Lengál, Olli Saarikivi, Margus Veanes, and Tomáš Vojnar
(Brno University of Technology, Czechia; Microsoft, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p480-p doi:10.1145/3428286

Feedback-Driven Semi-supervised Synthesis of Program Transformations
Xiang Gao, Shraddha Barke, Arjun Radhakrishna, Gustavo Soares, Sumit Gulwani, Alan Leung, Nachiappan Nagappan, and Ashish Tiwari
(National University of Singapore, Singapore; University of California at San Diego, USA; Microsoft, USA; Microsoft Research, USA)

Publisher's Version Video Article: oopsla20main-p494-p doi:10.1145/3428287

Contextual Dispatch for Function Specialization
Olivier Flückiger, Guido Chari, Ming-Ho Yee, Jan Ječmen, Jakob Hain, and Jan Vitek
(Northeastern University, USA; Asapp, Argentina; Czech Technical University, Czechia)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p502-p doi:10.1145/3428288

Counterexample-Guided Correlation Algorithm for Translation Validation
Shubhani Gupta, Abhishek Rose, and Sorav Bansal
(IIT Delhi, India)

Publisher's Version Video Artifacts Functional Artifacts Reusable Article: oopsla20main-p509-p doi:10.1145/3428289

Adding Interactive Visual Syntax to Textual Code
Leif Andersen, Michael Ballantyne, and Matthias Felleisen
(Northeastern University, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p510-p doi:10.1145/3428290

Revisiting Iso-Recursive Subtyping
Yaoda Zhou, Bruno C. d. S. Oliveira, and Jinxu Zhao
(University of Hong Kong, China)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p512-p doi:10.1145/3428291

Guiding Dynamic Programing via Structural Probability for Accelerating Programming by Example
Ruyi Ji, Yican Sun, Yingfei Xiong, and Zhenjiang Hu
(Peking University, China)

Publisher's Version Video Article: oopsla20main-p515-p doi:10.1145/3428292

Neural Reverse Engineering of Stripped Binaries using Augmented Control Flow Graphs
Yaniv David, Uri Alon, and Eran Yahav
(Technion, Israel)

Publisher's Version Published Artifact Video Article: oopsla20main-p526-p doi:10.1145/3428293

Foundations of Empirical Memory Consistency Testing
Jake Kirkham, Tyler Sorensen, Esin Tureci, and Margaret Martonosi
(Princeton University, USA; University of California at Santa Cruz, USA)

Publisher's Version Video Article: oopsla20main-p542-p doi:10.1145/3428294

Just-in-Time Learning for Bottom-Up Enumerative Synthesis
Shraddha Barke, Hila Peleg, and Nadia Polikarpova
(University of California at San Diego, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p583-p doi:10.1145/3428295

Gradual Verification of Recursive Heap Data Structures
Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine
(Carnegie Mellon University, USA; Jane Street, USA; University of Chile, Chile)

Publisher's Version Published Artifact Video Article: oopsla20main-p605-p doi:10.1145/3428296

Macros for Domain-Specific Languages
Michael Ballantyne, Alexis King, and Matthias Felleisen
(Northeastern University, USA; Northwestern University, USA)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Article: oopsla20main-p625-p doi:10.1145/3428297

Learning-Based Controlled Concurrency Testing
Suvam Mukherjee, Pantazis Deligiannis, Arpita Biswas, and Akash Lal
(Microsoft Research, India; Microsoft Research, USA; IISc Bangalore, India)

Publisher's Version Published Artifact Video Artifacts Available Artifacts Functional Artifacts Reusable Article: oopsla20main-p644-p doi:10.1145/3428298

TacTok: Semantics-Aware Proof Synthesis
Emily First, Yuriy Brun, and Arjun Guha
(University of Massachusetts at Amherst, USA)

Publisher's Version Published Artifact Video Article: oopsla20main-p664-p doi:10.1145/3428299

Koord: A Language for Programming and Verifying Distributed Robotics Application
Ritwika Ghosh, Chiao Hsieh, Sasa Misailovic, and Sayan Mitra
(University of Illinois at Urbana-Champaign, USA)

Publisher's Version Video Article: oopsla20main-p675-p doi:10.1145/3428300

Flow2Vec: Value-Flow-Based Precise Code Embedding
Yulei Sui, Xiao Cheng, Guanqin Zhang, and Haoyu Wang
(University of Technology Sydney, Australia; Beijing University of Posts and Telecommunications, China)

Publisher's Version Video Article: oopsla20main-p687-p doi:10.1145/3428301