OOPSLA – Journal Issue

Making Weak Memory Models Fair
Ori Lahav, Egor Namakonov, Jonas Oberhauser, Anton Podkopaev, and Viktor Vafeiadis
(Tel Aviv University, Israel; St. Petersburg University, Russia; JetBrains Research, Russia; Huawei, Germany; HSE University, Russia; MPI-SWS, Germany)

SecRSL: Security Separation Logic for C11 Release-Acquire Concurrency
Pengbo Yan and Toby Murray
(University of Melbourne, Australia)

Semantic Programming by Example with Pre-trained Models
Gust Verbruggen, Vu Le, and Sumit Gulwani
(KU Leuven, Belgium; Microsoft, USA)

Promises Are Made to Be Broken: Migrating R to Strict Semantics
Aviral Goel, Jan Ječmen, Sebastián Krynski, Olivier Flückiger, and Jan Vitek
(Northeastern University, USA; Czech Technical University, Czechia)

Efficient Compilation of Algebraic Effect Handlers
Georgios Karachalias, Filip Koprivec, Matija Pretnar, and Tom Schrijvers
(Tweag, France; University of Ljubljana, Slovenia; Institute of Mathematics, Physics, and Mechanics, Slovenia; KU Leuven, Belgium)

Safer at Any Speed: Automatic Context-Aware Safety Enhancement for Rust
Natalie Popescu, Ziyang Xu, Sotiris Apostolakis, David I. August, and Amit Levy
(Princeton University, USA; Google, USA)

Synthesizing Contracts Correct Modulo a Test Generator
Angello Astorga, Shambwaditya Saha, Ahmad Dinkins, Felicia Wang, P. Madhusudan, and Tao Xie
(University of Illinois at Urbana-Champaign, USA; Tufts University, USA; Peking University, China)

Synbit: Synthesizing Bidirectional Programs using Unidirectional Sketches
Masaomi Yamaguchi, Kazutaka Matsuda, Cristina David, and Meng Wang
(Tohoku University, Japan; University of Bristol, UK)

SimTyper: Sound Type Inference for Ruby using Type Equality Prediction
Milod Kazerounian, Jeffrey S. Foster, and Bonan Min
(University of Maryland at College Park, USA; Tufts University, USA; Raytheon BBN Technologies, USA)

ECROs: Building Global Scale Systems from Sequential Code
Kevin De Porre, Carla Ferreira, Nuno Preguiça, and Elisa Gonzalez Boix
(Vrije Universiteit Brussel, Belgium; NOVA School of Science and Technology, Portugal)

Label Dependent Lambda Calculus and Gradual Typing
Weili Fu, Fabian Krause, and Peter Thiemann
(University of Freiburg, Germany)

Efficient Automatic Scheduling of Imaging and Vision Pipelines for the GPU
Luke Anderson, Andrew Adams, Karima Ma, Tzu-Mao Li, Tian Jin, and Jonathan Ragan-Kelley
(Massachusetts Institute of Technology, USA; Adobe, USA; University of California at San Diego, USA)

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

Solver-Based Gradual Type Migration
Luna Phipps-Costin, Carolyn Jane Anderson, Michael Greenberg, and Arjun Guha
(University of Massachusetts at Amherst, USA; Wellesley College, USA; Stevens Institute of Technology, USA; Northeastern University, USA)

UDF to SQL Translation through Compositional Lazy Inductive Synthesis
Guoqiang Zhang, Yuanchao Xu, Xipeng Shen, and Işıl Dillig
(North Carolina State University, USA; University of Texas at Austin, USA)

Verifying Concurrent Multicopy Search Structures
Nisarg Patel, Siddharth Krishna, Dennis Shasha, and Thomas Wies
(New York University, USA; Microsoft Research, UK)

Compiling with Continuations, Correctly
Zoe Paraskevopoulou and Anvay Grover
(Northeastern University, USA; University of Wisconsin-Madison, USA)

Statically Bounded-Memory Delayed Sampling for Probabilistic Streams
Eric Atkinson, Guillaume Baudart, Louis Mandel, Charles Yuan, and Michael Carbin
(Massachusetts Institute of Technology, USA; Inria, France; ENS, France; PSL University, France; IBM Research, USA)

Data-Driven Abductive Inference of Library Specifications
Zhe Zhou, Robert Dickerson, Benjamin Delaware, and Suresh Jagannathan
(Purdue University, USA)

Formal Verification of High-Level Synthesis
Yann Herklotz, James D. Pollard, Nadesh Ramanathan, and John Wickerson
(Imperial College London, UK)

Program Analysis via Efficient Symbolic Abstraction
Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang
(Hong Kong University of Science and Technology, China; Ant Group, China)

Rewrite Rule Inference Using Equality Saturation
Chandrakana Nandi, Max Willsey, Amy Zhu, Yisu Remy Wang, Brett Saiki, Adam Anderson, Adriana Schulz, Dan Grossman, and Zachary Tatlock
(University of Washington, USA)

The Semantics of Shared Memory in Intel CPU/FPGA Systems
Dan Iorga, Alastair F. Donaldson, Tyler Sorensen, and John Wickerson
(Imperial College London, UK; University of California at Santa Cruz, USA)

Translating C to Safer Rust
Mehmet Emre, Ryan Schroeder, Kyle Dewey, and Ben Hardekopf
(University of California at Santa Barbara, USA; California State University at Northridge, USA)

One Down, 699 to Go: or, Synthesising Compositional Desugarings
Sándor Bartha, James Cheney, and Vaishak Belle
(University of Edinburgh, UK; Alan Turing Institute, UK)

Well-Typed Programs Can Go Wrong: A Study of Typing-Related Bugs in JVM Compilers
Stefanos Chaliasos, Thodoris Sotiropoulos, Georgios-Petros Drosos, Charalambos Mitropoulos, Dimitris Mitropoulos, and Diomidis Spinellis
(Athens University of Economics and Business, Greece; Technical University of Crete, Greece; University of Athens, Greece; Delft University of Technology, Netherlands)

A Multiparty Session Typing Discipline for Fault-Tolerant Event-Driven Distributed Programming
Malte Viering, Raymond Hu, Patrick Eugster, and Lukasz Ziarek
(TU Darmstadt, Germany; Queen Mary University of London, UK; USI Lugano, Switzerland; Purdue University, USA; University at Buffalo, USA)

What We Eval in the Shadows: A Large-Scale Study of Eval in R Programs
Aviral Goel, Pierre Donat-Bouillud, Filip Křikava, Christoph M. Kirsch, and Jan Vitek
(Northeastern University, USA; Czech Technical University, Czechia; University of Salzburg, Austria)

Gradually Structured Data
Stefan Malewski, Michael Greenberg, and Éric Tanter
(University of Chile, Chile; Stevens Institute of Technology, USA; IMFD, Chile)

Info

Transitioning from Structural to Nominal Code with Efficient Gradual Typing
Fabian Muehlboeck and Ross Tate
(IST Austria, Austria; Cornell University, USA)

Info

Compilation of Sparse Array Programming Models
Rawn Henry, Olivia Hsu, Rohan Yadav, Stephen Chou, Kunle Olukotun, Saman Amarasinghe, and Fredrik Kjolstad
(Massachusetts Institute of Technology, USA; Stanford University, USA)

Info

SpecSafe: Detecting Cache Side Channels in a Speculative World
Robert Brotzman, Danfeng Zhang, Mahmut Taylan Kandemir, and Gang Tan
(Pennsylvania State University, USA)

Coarsening Optimization for Differentiable Programming
Xipeng Shen, Guoqiang Zhang, Irene Dea, Samantha Andow, Emilio Arroyo-Fang, Neal Gafter, Johann George, Melissa Grueter, Erik Meijer, Olin Grigsby Shivers, Steffi Stumpos, Alanna Tempest, Christy Warden, and Shannon Yang
(North Carolina State University, USA; Facebook, USA)

Specifying and Testing GPU Workgroup Progress Models
Tyler Sorensen, Lucas F. Salvador, Harmit Raval, Hugues Evrard, John Wickerson, Margaret Martonosi, and Alastair F. Donaldson
(University of California at Santa Cruz, USA; Princeton University, USA; Google, USA; Imperial College London, UK)

MonkeyDB: Effectively Testing Correctness under Weak Isolation Levels
Ranadeep Biswas, Diptanshu Kakwani, Jyothi Vedurada, Constantin Enea, and Akash Lal
(Informal Systems, France; Microsoft, India; IIT Hyderabad, India; IRIF, France; University of Paris, France; CNRS, France; Microsoft Research, India)

Durable Functions: Semantics for Stateful Serverless
Sebastian Burckhardt, Chris Gillum, David Justo, Konstantinos Kallas, Connor McMahon, and Christopher S. Meiklejohn
(Microsoft Research, USA; Microsoft Azure, USA; University of Pennsylvania, USA; Carnegie Mellon University, USA)

Gauss: Program Synthesis by Reasoning over Graphs
Rohan Bavishi, Caroline Lemieux, Koushik Sen, and Ion Stoica
(University of California at Berkeley, USA)

A Type System for Extracting Functional Specifications from Memory-Safe Imperative Programs
Paul He, Eddy Westbrook, Brent Carmer, Chris Phifer, Valentin Robert, Karl Smeltzer, Andrei Ştefănescu, Aaron Tomb, Adam Wick, Matthew Yacavone, and Steve Zdancewic
(University of Pennsylvania, USA; Galois, USA)

Copy-and-Patch Compilation: A Fast Compilation Algorithm for High-Level Languages and Bytecode
Haoran Xu and Fredrik Kjolstad
(Stanford University, USA)

Info

Study of the Subtyping Machine of Nominal Subtyping with Variance
Ori Roth
(Technion, Israel)

Dynaplex: Analyzing Program Complexity using Dynamically Inferred Recurrence Relations
Didier Ishimwe, KimHao Nguyen, and ThanhVu Nguyen
(University of Nebraska-Lincoln, USA; George Mason University, USA)

Reachability Types: Tracking Aliasing and Separation in Higher-Order Functional Programs
Yuyan Bao, Guannan Wei, Oliver Bračevac, Yuxuan Jiang, Qiyang He, and Tiark Rompf
(University of Waterloo, Canada; Purdue University, USA)

Static Detection of Silent Misconfigurations with Deep Interaction Analysis
Jialu Zhang, Ruzica Piskac, Ennan Zhai, and Tianyin Xu
(Yale University, USA; Alibaba Group, USA; University of Illinois at Urbana-Champaign, USA)

Interpretable Noninterference Measurement and Its Application to Processor Designs
Ziqiao Zhou and Michael K. Reiter
(Microsoft Research, USA; Duke University, USA)

Info

Reconciling Optimization with Secure Compilation
Son Tuan Vu, Albert Cohen, Arnaud De Grandmaison, Christophe Guillon, and Karine Heydemann
(Sorbonne University, France; CNRS, France; LIP6, France; Google, France; ARM, France; STMicroelectronics, France)

Scalability and Precision by Combining Expressive Type Systems and Deductive Verification
Florian Lanzinger, Alexander Weigl, Mattias Ulbrich, and Werner Dietl
(KIT, Germany; University of Waterloo, Canada)

VESPA: Static Profiling for Binary Optimization
Angélica Aparecida Moreira, Guilherme Ottoni, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Facebook, USA)

Modular Specification and Verification of Closures in Rust
Fabian Wolff, Aurel Bílý, Christoph Matheja, Peter Müller, and Alexander J. Summers
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Rich Specifications for Ethereum Smart Contract Verification
Christian Bräm, Marco Eilers, Peter Müller, Robin Sierra, and Alexander J. Summers
(ETH Zurich, Switzerland; University of British Columbia, Canada)

Making Pointer Analysis More Precise by Unleashing the Power of Selective Context Sensitivity
Tian Tan, Yue Li, Xiaoxing Ma, Chang Xu, and Yannis Smaragdakis
(Nanjing University, China; University of Athens, Greece)

LXM: Better Splittable Pseudorandom Number Generators (and Almost as Fast)
Guy L. Steele Jr. and Sebastiano Vigna
(Oracle Labs, USA; University of Milan, Italy)

Permchecker: A Toolchain for Debugging Memory Managers with Typestate
Karl Cronburg and Samuel Z. Guyer
(Tufts University, USA)

Type Stability in Julia: Avoiding Performance Pathologies in JIT Compilation
Artem Pelenitsyn, Julia Belyakova, Benjamin Chung, Ross Tate, and Jan Vitek
(Northeastern University, USA; Cornell University, USA; Czech Technical University, Czechia)

Info

A Derivative-Based Parser Generator for Visibly Pushdown Grammars
Xiaodong Jia, Ashish Kumar, and Gang Tan
(Pennsylvania State University, USA)

Generative Type-Aware Mutation for Testing SMT Solvers
Jiwon Park, Dominik Winterer, Chengyu Zhang, and Zhendong Su
(École Polytechnique, France; ETH Zurich, Switzerland; East China Normal University, China)

LooPy: Interactive Program Synthesis with Control Structures
Kasra Ferdowsifard, Shraddha Barke, Hila Peleg, Sorin Lerner, and Nadia Polikarpova
(University of California at San Diego, USA; Technion, Israel)

Not So Fast: Understanding and Mitigating Negative Impacts of Compiler Optimizations on Code Reuse Gadget Sets
Michael D. Brown, Matthew Pruett, Robert Bigelow, Girish Mururu, and Santosh Pande
(Georgia Institute of Technology, USA)

How Statically-Typed Functional Programmers Write Code
Justin Lubin and Sarah E. Chasins
(University of California at Berkeley, USA)

Fully Automated Functional Fuzzing of Android Apps for Detecting Non-crashing Logic Bugs
Ting Su, Yichen Yan, Jue Wang, Jingling Sun, Yiheng Xiong, Geguang Pu, Ke Wang, and Zhendong Su
(East China Normal University, China; Nanjing University, China; Visa Research, USA; ETH Zurich, Switzerland)

QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
Nouraldin Jaber, Christopher Wagner, Swen Jacobs, Milind Kulkarni, and Roopsha Samanta
(Purdue University, USA; CISPA, Germany)

Multi-modal Program Inference: A Marriage of Pre-trained Language Models and Component-Based Synthesis
Kia Rahmani, Mohammad Raza, Sumit Gulwani, Vu Le, Daniel Morris, Arjun Radhakrishna, Gustavo Soares, and Ashish Tiwari
(Purdue University, USA; Microsoft, USA)

Compacting Points-To Sets through Object Clustering
Mohamad Barbar and Yulei Sui
(University of Technology Sydney, Australia; CSIRO’s Data61, Australia)

Automatic Migration from Synchronous to Asynchronous JavaScript APIs
Satyajit Gokhale, Alexi Turcotte, and Frank Tip
(Northeastern University, USA)

APIfix: Output-Oriented Program Synthesis for Combating Breaking Changes in Libraries
Xiang Gao, Arjun Radhakrishna, Gustavo Soares, Ridwan Shariffdeen, Sumit Gulwani, and Abhik Roychoudhury
(National University of Singapore, Singapore; Microsoft, USA)

FPL: Fast Presburger Arithmetic through Transprecision
Arjun Pitchanathan, Christian Ulmann, Michel Weber, Torsten Hoefler, and Tobias Grosser
(IIIT Hyderabad, India; ETH Zurich, Switzerland; University of Edinburgh, UK)

Symbolic Value-Flow Static Analysis: Deep, Precise, Complete Modeling of Ethereum Smart Contracts
Yannis Smaragdakis, Neville Grech, Sifis Lagouvardos, Konstantinos Triantafyllou, and Ilias Tsatiris
(University of Athens, Greece; University of Malta, Malta)

The Reads-From Equivalence for the TSO and PSO Memory Models
Truc Lam Bui, Krishnendu Chatterjee, Tushar Gautam, Andreas Pavlogiannis, and Viktor Toman
(Comenius University Bratislava, Slovakia; IST Austria, Austria; IIT Bombay, India; Aarhus University, Denmark)

JavaDL: Automatically Incrementalizing Java Bug Pattern Detection
Alexandru Dura, Christoph Reichenbach, and Emma Söderberg
(Lund University, Sweden)

Programming and Execution Models for Parallel Bounded Exhaustive Testing
Nader Al Awar, Kush Jain, Christopher J. Rossbach, and Milos Gligoric
(University of Texas at Austin, USA; Katana Graph, USA)

Generalizable Synthesis through Unification
Ruyi Ji, Jingtao Xia, Yingfei Xiong, and Zhenjiang Hu
(Peking University, China)