OOPSLA 2020
Proceedings of the ACM on Programming Languages, Volume 4, Number OOPSLA
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 4, Number OOPSLA, November 16–20, 2020, Virtual, USA

OOPSLA – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message

Papers

Fixpoints for the Masses: Programming with First-Class Datalog Constraints
Magnus Madsen ORCID logo and Ondřej Lhoták ORCID logo
(Aarhus University, Denmark; University of Waterloo, Canada)
Publisher's Version Video
Effects as Capabilities: Effect Handlers and Lightweight Effect Polymorphism
Jonathan Immanuel Brachthäuser, Philipp Schuster ORCID logo, and Klaus Ostermann ORCID logo
(EPFL, Switzerland; University of Tübingen, Germany)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
A Systematic Approach to Deriving Incremental Type Checkers
André Pacak ORCID logo, Sebastian ErdwegORCID logo, and Tamás Szabó
(University of Mainz, Germany; itemis, Germany)
Publisher's Version Video
Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam MorrisonORCID logo, Aleksandar Nanevski ORCID logo, Noam Rinetzky ORCID logo, and Sharon Shoham ORCID logo
(Tel Aviv University, Israel; University of Paris Diderot, France; IMDEA Software Institute, Spain)
Publisher's Version Video
Certified and Efficient Instruction Scheduling: Application to Interlocked VLIW Processors
Cyril Six, Sylvain BoulméORCID logo, and David MonniauxORCID logo
(Kalray, France; Grenoble Alps University, France; CNRS, France; Grenoble INP, France; VERIMAG, France)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
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
Semiring Optimizations: Dynamic Elision of Expressions with Identity and Absorbing Elements
Guilherme Vieira Leobas and Fernando Magno Quintão Pereira ORCID logo
(Federal University of Minas Gerais, Brazil)
Publisher's Version Video Info
Can Advanced Type Systems Be Usable? An Empirical Study of Ownership, Assets, and Typestate in Obsidian
Michael CoblenzORCID logo, Jonathan AldrichORCID logo, Brad A. MyersORCID logo, and Joshua SunshineORCID logo
(Carnegie Mellon University, USA)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
Assertion-Based Optimization of Quantum Programs
Thomas Häner, Torsten Hoefler ORCID logo, and Matthias Troyer
(ETH Zurich, Switzerland; Microsoft, USA)
Publisher's Version Video
Multiparty Motion Coordination: From Choreographies to Robotics Programs
Rupak Majumdar ORCID logo, Nobuko Yoshida ORCID logo, and Damien ZuffereyORCID logo
(MPI-SWS, Germany; Imperial College London, UK)
Publisher's Version Video Artifacts Functional
Automated Policy Synthesis for System Call Sandboxing
Shankara Pailoor ORCID logo, Xinyu Wang ORCID logo, Hovav Shacham, and Isil Dillig ORCID logo
(University of Texas at Austin, USA; University of Michigan, USA)
Publisher's Version Video
How Do Programmers Use Unsafe Rust?
Vytautas Astrauskas, Christoph Matheja, Federico Poli, Peter Müller ORCID logo, and Alexander J. Summers ORCID logo
(ETH Zurich, Switzerland; University of British Columbia, Canada)
Publisher's Version Video
Learning Semantic Program Embeddings with Graph Interval Neural Network
Yu Wang, Ke Wang ORCID logo, Fengjuan Gao, and Linzhang Wang ORCID logo
(Nanjing University, China; Visa Research, USA)
Publisher's Version Video
Mossad: Defeating Software Plagiarism Detection
Breanna Devore-McDonald and Emery D. Berger ORCID logo
(University of Massachusetts at Amherst, USA)
Publisher's Version Video
Handling Bidirectional Control Flow
Yizhou ZhangORCID logo, Guido SalvaneschiORCID logo, and Andrew C. Myers ORCID logo
(University of Waterloo, Canada; University of St. Gallen, Switzerland; Cornell University, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Scaling Exact Inference for Discrete Probabilistic Programs
Steven Holtzen, Guy Van den BroeckORCID logo, and Todd Millstein ORCID logo
(University of California at Los Angeles, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Formulog: Datalog for SMT-Based Static Analysis
Aaron Bembenek ORCID logo, Michael Greenberg ORCID logo, and Stephen Chong ORCID logo
(Harvard University, USA; Pomona College, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Precise Inference of Expressive Units of Measurement Types
Tongtong Xiang ORCID logo, Jeff Y. Luo, and Werner DietlORCID logo
(University of Waterloo, Canada)
Publisher's Version Video Info Artifacts Functional
WATCHER: In-Situ Failure Diagnosis
Hongyu Liu, Sam Silvestro ORCID logo, Xiangyu ZhangORCID logo, Jian Huang ORCID logo, and Tongping Liu ORCID logo
(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
A Model for Detecting Faults in Build Specifications
Thodoris Sotiropoulos ORCID logo, Stefanos Chaliasos, Dimitris Mitropoulos, and Diomidis Spinellis ORCID logo
(Athens University of Economics and Business, Greece)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Guided Linking: Dynamic Linking without the Costs
Sean Bartell ORCID logo, Will DietzORCID logo, and Vikram S. AdveORCID logo
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Satune: Synthesizing Efficient SAT Encoders
Hamed GorjiaraORCID logo, Guoqing Harry Xu ORCID logo, and Brian Demsky ORCID logo
(University of California at Irvine, USA; University of California at Los Angeles, USA)
Publisher's Version Video Info
Exposing Cache Timing Side-Channel Leaks through Out-of-Order Symbolic Execution
Shengjian Guo ORCID logo, Yueqi Chen, Jiyong Yu, Meng Wu, Zhiqiang ZuoORCID logo, 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
Statically Verified Refinements for Multiparty Protocols
Fangyi Zhou ORCID logo, Francisco Ferreira ORCID logo, Raymond Hu ORCID logo, Rumyana Neykova ORCID logo, and Nobuko Yoshida ORCID logo
(Imperial College London, UK; University of Hertfordshire, UK; Brunel University London, UK)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Featherweight Go
Robert Griesemer, Raymond Hu ORCID logo, Wen Kokke ORCID logo, Julien Lange ORCID logo, Ian Lance Taylor, Bernardo Toninho ORCID logo, Philip Wadler ORCID logo, and Nobuko Yoshida ORCID logo
(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 Video Artifacts Functional Artifacts Reusable
Projection-Based Runtime Assertions for Testing and Debugging Quantum Programs
Gushu LiORCID logo, Li Zhou, Nengkun Yu ORCID logo, Yufei Ding ORCID logo, Mingsheng Ying, and Yuan Xie ORCID logo
(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
Persistent Owicki-Gries Reasoning: A Program Logic for Reasoning about Persistent Programs on Intel-x86
Azalea Raad, Ori LahavORCID logo, and Viktor VafeiadisORCID logo
(MPI-SWS, Germany; Imperial College London, UK; Tel Aviv University, Israel)
Publisher's Version Video
Igloo: Soundly Linking Compositional Refinement and Separation Logic for Distributed System Verification
Christoph Sprenger, Tobias Klenze, Marco Eilers ORCID logo, Felix A. Wolf, Peter Müller ORCID logo, Martin Clochard, and David Basin ORCID logo
(ETH Zurich, Switzerland)
Publisher's Version Video Artifacts Functional Artifacts Reusable
DiffStream: Differential Output Testing for Stream Processing Programs
Konstantinos KallasORCID logo, Filip Niksic, Caleb Stanford ORCID logo, and Rajeev AlurORCID logo
(University of Pennsylvania, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Polymorphic Types and Effects with Boolean Unification
Magnus Madsen ORCID logo and Jaco van de Pol ORCID logo
(Aarhus University, Denmark)
Publisher's Version Video
CAMP: Cost-Aware Multiparty Session Protocols
David Castro-Perez ORCID logo and Nobuko Yoshida ORCID logo
(Imperial College London, UK)
Publisher's Version Video Artifacts Functional Artifacts Reusable
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 Video Artifacts Functional
Automatic and Efficient Variability-Aware Lifting of Functional Programs
Ramy Shahin and Marsha Chechik ORCID logo
(University of Toronto, Canada)
Publisher's Version Video
A Sparse Iteration Space Transformation Framework for Sparse Tensor Algebra
Ryan Senanayake ORCID logo, Changwan Hong, Ziheng Wang, Amalee Wilson, Stephen ChouORCID logo, Shoaib Kamil, Saman AmarasingheORCID logo, and Fredrik KjolstadORCID logo
(Reservoir Labs, USA; Massachusetts Institute of Technology, USA; Stanford University, USA; Adobe Research, USA)
Publisher's Version Video
Programming with a Read-Eval-Synth Loop
Hila Peleg, Roi Gabay, Shachar Itzhaky ORCID logo, and Eran Yahav
(University of California at San Diego, USA; Technion, Israel; Codota, Israel)
Publisher's Version Video Video Artifacts Functional Artifacts Reusable
LiveDroid: Identifying and Preserving Mobile App State in Volatile Runtime Environments
Umar Farooq ORCID logo, Zhijia Zhao ORCID logo, Manu Sridharan ORCID logo, and Iulian Neamtiu
(University of California at Riverside, USA; New Jersey Institute of Technology, USA)
Publisher's Version Video
Towards a Unified Proof Framework for Automated Fixpoint Reasoning using Matching Logic
Xiaohong ChenORCID logo, Minh-Thai Trinh ORCID logo, Nishant Rodrigues, Lucas Peña ORCID logo, and Grigore Roşu ORCID logo
(University of Illinois at Urbana-Champaign, USA; Advanced Digital Sciences Center, Singapore)
Publisher's Version Video
Adversarial Examples for Models of Code
Noam Yefet, Uri Alon, and Eran Yahav
(Technion, Israel)
Publisher's Version Video Info
Towards a Formal Foundation of Intermittent Computing
Milijana Surbatovich ORCID logo, Brandon Lucia ORCID logo, and Limin Jia ORCID logo
(Carnegie Mellon University, USA)
Publisher's Version Video
Compiling Symbolic Execution with Staging and Algebraic Effects
Guannan Wei, Oliver Bračevac, Shangyin Tan, and Tiark Rompf ORCID logo
(Purdue University, USA)
Publisher's Version Video
Testing Differential Privacy with Dual Interpreters
Hengchu Zhang, Edo Roth, Andreas Haeberlen, Benjamin C. Pierce ORCID logo, and Aaron Roth
(University of Pennsylvania, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
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
Dynamic Dispatch of Context-Sensitive Optimizations
Gabriel Poesia and Fernando Magno Quintão Pereira ORCID logo
(Stanford University, USA; Federal University of Minas Gerais, Brazil)
Publisher's Version Video
Eliminating Abstraction Overhead of Java Stream Pipelines using Ahead-of-Time Program Optimization
Anders MøllerORCID logo and Oskar Haarklou Veileborg
(Aarhus University, Denmark)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
Build Scripts with Perfect Dependencies
Sarah Spall, Neil Mitchell, and Sam Tobin-Hochstadt ORCID logo
(Indiana University, USA; Facebook, UK)
Publisher's Version Video
Deductive Optimization of Relational Data Storage
John FeserORCID logo, Sam Madden, Nan Tang, and Armando Solar-Lezama ORCID logo
(Massachusetts Institute of Technology, USA; QCRI HBKU, Qatar)
Publisher's Version Video
Program Equivalence for Assisted Grading of Functional Programs
Joshua Clune ORCID logo, Vijay Ramamurthy, Ruben Martins, and Umut A. Acar ORCID logo
(Carnegie Mellon University, USA)
Publisher's Version Video
A Modular Cost Analysis for Probabilistic Programs
Martin Avanzini ORCID logo, Georg Moser ORCID logo, and Michael Schaper
(Inria, France; University of Innsbruck, Austria)
Publisher's Version Video
Geometry Types for Graphics Programming
Dietrich Geisler, Irene YoonORCID logo, Aditi Kabra, Horace He, Yinnon Sanders, and Adrian SampsonORCID logo
(Cornell University, USA; University of Pennsylvania, USA; Carnegie Mellon University, USA)
Publisher's Version Video Info Artifacts Functional
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
A Type-and-Effect System for Object Initialization
Fengyun Liu, Ondřej Lhoták ORCID logo, Aggelos Biboudis, Paolo G. Giarrusso, and Martin Odersky ORCID logo
(EPFL, Switzerland; University of Waterloo, Canada; Delft University of Technology, Netherlands)
Publisher's Version Video Artifacts Functional
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
Dataflow-Based Pruning for Speeding up Superoptimization
Manasij Mukherjee ORCID logo, Pranav Kant, Zhengyang Liu, and John Regehr ORCID logo
(University of Utah, USA)
Publisher's Version Video
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
Learning Graph-Based Heuristics for Pointer Analysis without Handcrafting Application-Specific Features
Minseok Jeon ORCID logo, Myungho Lee, and Hakjoo Oh ORCID logo
(Korea University, South Korea)
Publisher's Version Video Info Artifacts Functional
Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications
Arjen Rouvoet ORCID logo, Hendrik van Antwerpen ORCID logo, Casper Bach Poulsen ORCID logo, Robbert KrebbersORCID logo, and Eelco Visser ORCID logo
(Delft University of Technology, Netherlands)
Publisher's Version Video Info Artifacts Functional
Designing Types for R, Empirically
Alexi Turcotte, Aviral Goel, Filip Křikava ORCID logo, and Jan Vitek ORCID logo
(Northeastern University, USA; Czech Technical University, Czechia)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Shiftry: RNN Inference in 2KB of RAM
Aayan Kumar, Vivek Seshadri ORCID logo, and Rahul Sharma ORCID logo
(Microsoft Research, India)
Publisher's Version Video
StreamQL: A Query Language for Processing Streaming Time Series
Lingkun KongORCID logo and Konstantinos Mamouras ORCID logo
(Rice University, USA)
Publisher's Version Video Artifacts Functional
Incremental Predicate Analysis for Regression Verification
Qianshan Yu ORCID logo, Fei HeORCID logo, and Bow-Yaw Wang
(Tsinghua University, China; Academia Sinica, Taiwan)
Publisher's Version Video
Perfectly Parallel Fairness Certification of Neural Networks
Caterina UrbanORCID logo, Maria ChristakisORCID logo, Valentin Wüstholz ORCID logo, and Fuyuan Zhang
(Inria, France; ENS, France; CNRS, France; PSL University, France; MPI-SWS, Germany; ConsenSys, Germany)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Fuzzing Channel-Based Concurrency Runtimes using Types and Effects
Quentin Stiévenart and Magnus Madsen ORCID logo
(Vrije Universiteit Brussel, Belgium; Aarhus University, Denmark)
Publisher's Version Video
Detecting Locations in JavaScript Programs Affected by Breaking Library Changes
Anders MøllerORCID logo, Benjamin Barslev Nielsen, and Martin Toldam Torp
(Aarhus University, Denmark)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
Rethinking Safe Consistency in Distributed Object-Oriented Programming
Mirko Köhler ORCID logo, Nafise Eskandani, Pascal WeisenburgerORCID logo, Alessandro Margara, and Guido SalvaneschiORCID logo
(TU Darmstadt, Germany; Politecnico di Milano, Italy; University of St. Gallen, Switzerland)
Publisher's Version Video
DynamiTe: Dynamic Termination and Non-termination Proofs
Ton Chanh Le ORCID logo, Timos Antonopoulos ORCID logo, Parisa Fathololumi, Eric Koskinen ORCID logo, and ThanhVu NguyenORCID logo
(Stevens Institute of Technology, USA; Yale University, USA; University of Nebraska-Lincoln, USA)
Publisher's Version Video
Precise Static Modeling of Ethereum “Memory”
Sifis Lagouvardos ORCID logo, Neville Grech, Ilias Tsatiris ORCID logo, and Yannis Smaragdakis
(University of Athens, Greece)
Publisher's Version Video Artifacts Functional
Taming Type Annotations in Gradual Typing
John Peter Campora and Sheng Chen
(University of Louisiana at Lafayette, USA)
Publisher's Version Video
Inter-theory Dependency Analysis for SMT String Solvers
Minh-Thai Trinh ORCID logo, Duc-Hiep Chu, and Joxan JaffarORCID logo
(Advanced Digital Sciences Center, Singapore; National University of Singapore, Singapore)
Publisher's Version Video Artifacts Functional
On the Unusual Effectiveness of Type-Aware Operator Mutations for Testing SMT Solvers
Dominik Winterer, Chengyu Zhang ORCID logo, and Zhendong Su ORCID logo
(ETH Zurich, Switzerland; East China Normal University, China)
Publisher's Version Video
Pomsets with Preconditions: A Simple Model of Relaxed Memory
Radha Jagadeesan, Alan Jeffrey, and James RielyORCID logo
(DePaul University, USA; Mozilla Research, USA)
Publisher's Version Video
Fast Linear Programming through Transprecision Computing on Small and Sparse Data
Tobias Grosser, Theodoros Theodoridis ORCID logo, Maximilian Falkenstein, Arjun Pitchanathan, Michael Kruse, Manuel Rigger ORCID logo, Zhendong Su ORCID logo, and Torsten Hoefler
(University of Edinburgh, UK; ETH Zurich, Switzerland; IIIT Hyderabad, India; Argonne National Laboratory, USA)
Publisher's Version Video
Random Testing for C and C++ Compilers with YARPGen
Vsevolod Livinskii ORCID logo, Dmitry Babokin ORCID logo, and John Regehr ORCID logo
(University of Utah, USA; Intel Corporation, USA)
Publisher's Version Video
CompCertELF: Verified Separate Compilation of C Programs into ELF Object Files
Yuting Wang ORCID logo, Xiangzhe Xu, Pierre Wilke, and Zhong Shao ORCID logo
(Shanghai Jiao Tong University, China; Nanjing University, China; CentraleSupélec, France; Yale University, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Scalable and Serializable Networked Multi-actor Programming
Bo Sang, Patrick EugsterORCID logo, Gustavo Petri, Srivatsan Ravi ORCID logo, and Pierre-Louis Roman ORCID logo
(Purdue University, USA; Ant Group, USA; USI Lugano, Switzerland; TU Darmstadt, Germany; ARM Research, UK; University of Southern California, USA)
Publisher's Version Video
Termination Analysis for Evolving Programs: An Incremental Approach by Reusing Certified Modules
Fei HeORCID logo and Jitao Han
(Tsinghua University, China)
Publisher's Version Video
Programming and Reasoning with Partial Observability
Eric Atkinson ORCID logo and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Interactive Synthesis of Temporal Specifications from Examples and Natural Language
Ivan Gavran, Eva Darulova ORCID logo, and Rupak Majumdar ORCID logo
(MPI-SWS, Germany)
Publisher's Version Video Artifacts Functional Artifacts Reusable
A Large-Scale Longitudinal Study of Flaky Tests
Wing Lam, Stefan Winter, Anjiang Wei, Tao XieORCID logo, Darko MarinovORCID logo, and Jonathan Bell
(University of Illinois at Urbana-Champaign, USA; TU Darmstadt, Germany; Peking University, China; Northeastern University, USA)
Publisher's Version Video
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 Info
Do You Have Space for Dessert? A Verified Space Cost Semantics for CakeML Programs
Alejandro Gómez-Londoño, Johannes Åman Pohjola, Hira Taqdees SyedaORCID logo, Magnus O. MyreenORCID logo, 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
Digging for Fold: Synthesis-Aided API Discovery for Haskell
Michael B. JamesORCID logo, Zheng Guo ORCID logo, Ziteng Wang, Shivani Doshi, Hila Peleg, Ranjit JhalaORCID logo, and Nadia PolikarpovaORCID logo
(University of California at San Diego, USA)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Resolution as Intersection Subtyping via Modus Ponens
Koar Marntirosian, Tom SchrijversORCID logo, Bruno C. d. S. OliveiraORCID logo, and Georgios Karachalias ORCID logo
(KU Leuven, Belgium; University of Hong Kong, China; Tweag, France)
Publisher's Version Video Artifacts Functional Artifacts Reusable
World Age in Julia: Optimizing Method Dispatch in the Presence of Eval
Julia BelyakovaORCID logo, Benjamin Chung, Jack Gelinas, Jameson Nash, Ross TateORCID logo, and Jan VitekORCID logo
(Northeastern University, USA; Julia Computing, USA; Cornell University, USA; Czech Technical University, Czechia)
Publisher's Version Video Info
ιDOT: A DOT Calculus with Object Initialization
Ifaz Kabir, Yufeng Li, and Ondřej Lhoták ORCID logo
(University of Alberta, Canada; University of Waterloo, Canada)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Taming Callbacks for Smart Contract Modularity
Elvira Albert, Shelly Grossman, Noam Rinetzky, Clara Rodríguez-Núñez ORCID logo, Albert Rubio ORCID logo, and Mooly Sagiv
(Complutense University of Madrid, Spain; Tel Aviv University, Israel)
Publisher's Version Video
Testing Consensus Implementations using Communication Closure
Cezara Drăgoi, Constantin Enea, Burcu Kulahcioglu Ozkan, Rupak Majumdar ORCID logo, 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
Finding Bugs in Database Systems via Query Partitioning
Manuel Rigger ORCID logo and Zhendong Su ORCID logo
(ETH Zurich, Switzerland)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
Structure Interpretation of Text Formats
Sumit GulwaniORCID logo, Vu LeORCID logo, Arjun Radhakrishna ORCID logo, Ivan Radiček ORCID logo, and Mohammad Raza ORCID logo
(Microsoft, USA; Microsoft, Austria)
Publisher's Version Video
Programming at the Edge of Synchrony
Cezara Drăgoi, Josef Widder ORCID logo, and Damien ZuffereyORCID logo
(Inria, France; ENS, France; CNRS, France; PSL University, France; Informal Systems, France; Informal Systems, Austria; MPI-SWS, Germany)
Publisher's Version
Actor Concurrency Bugs: A Comprehensive Study on Symptoms, Root Causes, API Usages, and Differences
Mehdi BagherzadehORCID logo, Nicholas Fireman, Anas Shawesh, and Raffi KhatchadourianORCID logo
(Oakland University, USA; City University of New York, USA)
Publisher's Version Video
A Structural Model for Contextual Code Changes
Shaked Brody, Uri Alon, and Eran Yahav
(Technion, Israel)
Publisher's Version Video Info Artifacts Functional Artifacts Reusable
Verifying Replicated Data Types with Typeclass Refinements in Liquid Haskell
Yiyun Liu, James Parker, Patrick Redmond ORCID logo, Lindsey Kuper ORCID logo, Michael HicksORCID logo, and Niki VazouORCID logo
(University of Maryland at College Park, USA; University of California at Santa Cruz, USA; IMDEA Software Institute, Spain)
Publisher's Version Video Artifacts Functional
Unifying Execution of Imperative Generators and Declarative Specifications
Pengyu Nie ORCID logo, Marinela Parovic, Zhiqiang Zang ORCID logo, Sarfraz Khurshid, Aleksandar Milicevic, and Milos GligoricORCID logo
(University of Texas at Austin, USA; Microsoft, USA)
Publisher's Version Video
Regex Matching with Counting-Set Automata
Lenka Turoňová, Lukáš HolíkORCID logo, Ondřej Lengál ORCID logo, Olli Saarikivi ORCID logo, Margus VeanesORCID logo, and Tomáš VojnarORCID logo
(Brno University of Technology, Czechia; Microsoft, USA)
Publisher's Version Video Artifacts Functional
Feedback-Driven Semi-supervised Synthesis of Program Transformations
Xiang Gao, Shraddha BarkeORCID logo, Arjun Radhakrishna ORCID logo, Gustavo Soares ORCID logo, Sumit GulwaniORCID logo, 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 Video
Contextual Dispatch for Function Specialization
Olivier FlückigerORCID logo, Guido Chari, Ming-Ho Yee, Jan Ječmen ORCID logo, Jakob Hain, and Jan VitekORCID logo
(Northeastern University, USA; Asapp, Argentina; Czech Technical University, Czechia)
Publisher's Version Video Info Artifacts Functional
Counterexample-Guided Correlation Algorithm for Translation Validation
Shubhani Gupta, Abhishek Rose ORCID logo, and Sorav Bansal ORCID logo
(IIT Delhi, India)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Adding Interactive Visual Syntax to Textual Code
Leif AndersenORCID logo, Michael Ballantyne, and Matthias Felleisen ORCID logo
(Northeastern University, USA)
Publisher's Version Video Artifacts Functional
Revisiting Iso-Recursive Subtyping
Yaoda Zhou, Bruno C. d. S. OliveiraORCID logo, and Jinxu Zhao
(University of Hong Kong, China)
Publisher's Version Video Artifacts Functional Artifacts Reusable
Guiding Dynamic Programing via Structural Probability for Accelerating Programming by Example
Ruyi Ji ORCID logo, Yican Sun ORCID logo, Yingfei Xiong ORCID logo, and Zhenjiang Hu ORCID logo
(Peking University, China)
Publisher's Version Video Info
Neural Reverse Engineering of Stripped Binaries using Augmented Control Flow Graphs
Yaniv David, Uri Alon, and Eran Yahav
(Technion, Israel)
Publisher's Version Video Info
Foundations of Empirical Memory Consistency Testing
Jake Kirkham, Tyler SorensenORCID logo, Esin Tureci, and Margaret MartonosiORCID logo
(Princeton University, USA; University of California at Santa Cruz, USA)
Publisher's Version Video
Just-in-Time Learning for Bottom-Up Enumerative Synthesis
Shraddha BarkeORCID logo, Hila Peleg, and Nadia PolikarpovaORCID logo
(University of California at San Diego, USA)
Publisher's Version Video Artifacts Functional
Gradual Verification of Recursive Heap Data Structures
Jenna WiseORCID logo, Johannes Bader, Cameron Wong, Jonathan AldrichORCID logo, Éric TanterORCID logo, and Joshua SunshineORCID logo
(Carnegie Mellon University, USA; Jane Street, USA; University of Chile, Chile)
Publisher's Version Video Info
Macros for Domain-Specific Languages
Michael Ballantyne, Alexis King, and Matthias Felleisen ORCID logo
(Northeastern University, USA; Northwestern University, USA)
Publisher's Version Video Artifacts Functional
Learning-Based Controlled Concurrency Testing
Suvam MukherjeeORCID logo, Pantazis DeligiannisORCID logo, Arpita BiswasORCID logo, and Akash LalORCID logo
(Microsoft Research, India; Microsoft Research, USA; IISc Bangalore, India)
Publisher's Version Video Artifacts Functional Artifacts Reusable
TacTok: Semantics-Aware Proof Synthesis
Emily First ORCID logo, Yuriy BrunORCID logo, and Arjun Guha ORCID logo
(University of Massachusetts at Amherst, USA)
Publisher's Version Video Info
Koord: A Language for Programming and Verifying Distributed Robotics Application
Ritwika Ghosh, Chiao Hsieh ORCID logo, Sasa MisailovicORCID logo, and Sayan Mitra ORCID logo
(University of Illinois at Urbana-Champaign, USA)
Publisher's Version Video Info
Flow2Vec: Value-Flow-Based Precise Code Embedding
Yulei SuiORCID logo, Xiao Cheng, Guanqin Zhang, and Haoyu Wang
(University of Technology Sydney, Australia; Beijing University of Posts and Telecommunications, China)
Publisher's Version Video

proc time: 28.76