OOPSLA – Journal Issue

Probabilistic Verification of Fairness Properties via Concentration
Osbert Bastani, Xin Zhang, and Armando Solar-Lezama
(University of Pennsylvania, USA; Massachusetts Institute of Technology, USA)

Verifying Safety and Accuracy of Approximate Parallel Programs via Canonical Sequentialization
Vimuth Fernando, Keyur Joshi, and Sasa Misailovic
(University of Illinois at Urbana-Champaign, USA)

Qubit Allocation as a Combination of Subgraph Isomorphism and Token Swapping
Marcos Yukio Siraichi, Vinícius Fernandes dos Santos, Caroline Collange, and Fernando Magno Quintão Pereira
(Federal University of Minas Gerais, Brazil; Inria, France; University of Rennes, France; CNRS, France; IRISA, France)

Modular Verification of Heap Reachability Properties in Separation Logic
Arshavir Ter-Gabrielyan, Alexander J. Summers, and Peter Müller
(ETH Zurich, Switzerland)

Complete Monitors for Gradual Types
Ben Greenman, Matthias Felleisen, and Christos Dimoulas
(Northeastern University, USA; Northwestern University, USA)

TLA+ Model Checking Made Symbolic
Igor Konnov, Jure Kukovec, and Thanh-Hai Tran
(Inria, France; LORIA, France; University of Lorraine, France; CNRS, France; TU Vienna, Austria)

Value-Centric Dynamic Partial Order Reduction
Krishnendu Chatterjee, Andreas Pavlogiannis, and Viktor Toman
(IST Austria, Austria; EPFL, Switzerland)

Seq: A High-Performance Language for Bioinformatics
Ariya Shajii, Ibrahim Numanagić, Riyadh Baghdadi, Bonnie Berger, and Saman Amarasinghe
(Massachusetts Institute of Technology, USA)

Staged Abstract Interpreters: Fast and Modular Whole-Program Analysis via Meta-programming
Guannan Wei, Yuxuan Chen, and Tiark Rompf
(Purdue University, USA)

Derivative Grammars: A Symbolic Approach to Parsing with Derivatives
Ian Henriksen, Gianfranco Bilardi, and Keshav Pingali
(University of Texas at Austin, USA; University of Padua, Italy)

Efficient Lock-Free Durable Sets
Yoav Zuriel, Michal Friedman, Gali Sheffi, Nachshon Cohen, and Erez Petrank
(Technion, Israel; Amazon, Israel)

Modular Verification for Almost-Sure Termination of Probabilistic Programs
Mingzhang Huang, Hongfei Fu, Krishnendu Chatterjee, and Amir Kafshdar Goharshady
(Shanghai Jiao Tong University, China; East China Normal University, China; IST Austria, Austria)

IVT: An Efficient Method for Sharing Subtype Polymorphic Objects
Yu-Ping Wang, Xu-Qiang Hu, Zi-Xin Zou, Wende Tan, and Gang Tan
(Tsinghua University, China; Pennsylvania State University, USA)

Refinement Kinds: Type-Safe Programming with Practical Type-Level Computation
Luís Caires and Bernardo Toninho
(Nova University of Lisbon, Portugal; NOVA-LINCS, Portugal)

Program Synthesis with Algebraic Library Specifications
Benjamin Mariano, Josh Reese, Siyuan Xu, ThanhVu Nguyen, Xiaokang Qiu, Jeffrey S. Foster, and Armando Solar-Lezama
(University of Maryland at College Park, USA; Purdue University, USA; University of Nebraska-Lincoln, USA; Tufts University, USA; Massachusetts Institute of Technology, USA)

Weakening WebAssembly
Conrad Watt, Andreas Rossberg, and Jean Pichon-Pharabod
(University of Cambridge, UK; Dfinity Stiftung, Germany)

Generating a Fluent API with Syntax Checking from an LR Grammar
Tetsuro Yamazaki, Tomoki Nakamaru, Kazuhiro Ichikawa, and Shigeru Chiba
(University of Tokyo, Japan)

Weak Persistency Semantics from the Ground Up: Formalising the Persistency Semantics of ARMv8 and Transactional Models
Azalea Raad, John Wickerson, and Viktor Vafeiadis
(MPI-SWS, Germany; Imperial College London, UK)

DeepSEA: A Language for Certified System Software
Vilhelm Sjöberg, Yuyang Sang, Shu-chun Weng, and Zhong Shao
(Yale University, USA; CertiK, USA)

BDA: Practical Dependence Analysis for Binary Executables by Unbiased Whole-Program Path Sampling and Per-Path Abstract Interpretation
Zhuo Zhang, Wei You, Guanhong Tao, Guannan Wei, Yonghwi Kwon, and Xiangyu Zhang
(Purdue University, USA; Renmin University of China, China; University of Virginia, USA)

Asphalion: Trustworthy Shielding against Byzantine Faults
Ivana Vukotic, Vincent Rahli, and Paulo Esteves-Veríssimo
(University of Luxembourg, Luxembourg; University of Birmingham, UK)

Automatic Repair of Regular Expressions
Rong Pan, Qinheping Hu, Gaowei Xu, and Loris D'Antoni
(University of Texas at Austin, USA; University of Wisconsin-Madison, USA)

Static Analysis with Demand-Driven Value Refinement
Benno Stein, Benjamin Barslev Nielsen, Bor-Yuh Evan Chang, and Anders Møller
(University of Colorado Boulder, USA; Aarhus University, Denmark)

Relational Verification using Reinforcement Learning
Jia Chen, Jiayi Wei, Yu Feng, Osbert Bastani, and Isil Dillig
(University of Texas at Austin, USA; University of California at Santa Barbara, USA; University of Pennsylvania, USA)

A Formalization of Java’s Concurrent Access Modes
John Bender and Jens Palsberg
(University of California at Los Angeles, USA)

On the Fly Synthesis of Edit Suggestions
Anders Miltner, Sumit Gulwani, Vu Le, Alan Leung, Arjun Radhakrishna, Gustavo Soares, Ashish Tiwari, and Abhishek Udupa
(Princeton University, USA; Microsoft, USA)

A Fault-Tolerant Programming Model for Distributed Interactive Applications
Ragnar Mogk, Joscha Drechsler, Guido Salvaneschi, and Mira Mezini
(TU Darmstadt, Germany)

A Path to DOT: Formalizing Fully Path-Dependent Types
Marianna Rapoport and Ondřej Lhoták
(University of Waterloo, Canada)

Reliable and Fast DWARF-Based Stack Unwinding
Théophile Bastian, Stephen Kell, and Francesco Zappa Nardelli
(ENS, France; University of Kent, UK; Inria, France)

Leveraging Rust Types for Modular Specification and Verification
Vytautas Astrauskas, Peter Müller, Federico Poli, and Alexander J. Summers
(ETH Zurich, Switzerland)

Precision-Preserving Yet Fast Object-Sensitive Pointer Analysis with Partial Context Sensitivity
Jingbo Lu and Jingling Xue
(UNSW, Australia)

Formal Foundations of Serverless Computing
Abhinav Jangda, Donald Pinckney, Yuriy Brun, and Arjun Guha
(University of Massachusetts Amherst, USA)

Optimal Stateless Model Checking for Reads-From Equivalence under Sequential Consistency
Parosh Aziz Abdulla, Mohamed Faouzi Atig, Bengt Jonsson, Magnus Lång, Tuan Phong Ngo, and Konstantinos Sagonas
(Uppsala University, Sweden)

Modular Verification of Web Page Layout
Pavel Panchekha, Michael D. Ernst, Zachary Tatlock, and Shoaib Kamil
(University of Utah, USA; University of Washington, USA; Adobe, USA)

Aroma: Code Recommendation via Structural Code Search
Sifei Luan, Di Yang, Celeste Barnaby, Koushik Sen, and Satish Chandra
(Facebook, USA; University of California at Irvine, USA; University of California at Berkeley, USA)

On the Design, Implementation, and Use of Laziness in R
Aviral Goel and Jan Vitek
(Northeastern University, USA; Czech Technical University, Czechia)

Mergeable Replicated Data Types
Gowtham Kaki, Swarn Priya, KC Sivaramakrishnan, and Suresh Jagannathan
(Purdue University, USA; IIT Madras, India)

Compiler Fuzzing: How Much Does It Matter?
Michaël Marcozzi, Qiyi Tang, Alastair F. Donaldson, and Cristian Cadar
(Imperial College London, UK)

DProf: Distributed Profiler with Strong Guarantees
Zachary Benavides, Keval Vora, and Rajiv Gupta
(University of California at Riverside, USA; Simon Fraser University, Canada)

Precise Reasoning with Structured Time, Structured Heaps, and Collective Operations
Grégory M. Essertel, Guannan Wei, and Tiark Rompf
(Purdue University, USA)

Casting about in the Dark: An Empirical Study of Cast Operations in Java Programs
Luis Mastrangelo, Matthias Hauswirth, and Nathaniel Nystrom
(USI Lugano, Switzerland)

Getafix: Learning to Fix Bugs Automatically
Johannes Bader, Andrew Scott, Michael Pradel, and Satish Chandra
(Facebook, USA)

Generating Precise Error Specifications for C: A Zero Shot Learning Approach
Baijun Wu, John Peter Campora III, Yi He, Alexander Schlecht, and Sheng Chen
(University of Louisiana at Lafayette, USA)

Specifying Concurrent Programs in Separation Logic: Morphisms and Simulations
Aleksandar Nanevski, Anindya Banerjee, Germán Andrés Delbianco, and Ignacio Fábregas
(IMDEA Software Institute, Spain; IRIF, France; University of Paris, France)

Improving Bug Detection via Context-Based Code Representation Learning and Attention-Based Neural Networks
Yi Li, Shaohua Wang, Tien N. Nguyen, and Son Van Nguyen
(New Jersey Institute of Technology, USA; University of Texas at Dallas, USA)

Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild
Filip Křikava, Heather Miller, and Jan Vitek
(Czech Technical University, Czechia; Carnegie Mellon University, USA; Northeastern University, USA)

Optimization of Swift Protocols
Rajkishore Barik, Manu Sridharan, Murali Krishna Ramanathan, and Milind Chabbi
(Uber Technologies, USA; University of California at Riverside, USA)

On the Complexity of Checking Transactional Consistency
Ranadeep Biswas and Constantin Enea
(University of Paris, France; IRIF, France; CNRS, France)

System FR: Formalized Foundations for the Stainless Verifier
Jad Hamza, Nicolas Voirol, and Viktor Kunčak
(EPFL, Switzerland)

Language-Integrated Privacy-Aware Distributed Queries
Guido Salvaneschi, Mirko Köhler, Daniel Sokolowski, Philipp Haller, Sebastian Erdweg, and Mira Mezini
(TU Darmstadt, Germany; KTH, Sweden; Johannes Gutenberg University Mainz, Germany)

AutoPandas: Neural-Backed Generators for Program Synthesis
Rohan Bavishi, Caroline Lemieux, Roy Fox, Koushik Sen, and Ion Stoica
(University of California at Berkeley, USA; University of California at Irvine, USA)

Ryū Revisited: Printf Floating Point Conversion
Ulf Adams
(Google, Germany)

IntelliMerge: A Refactoring-Aware Software Merging Technique
Bo Shen, Wei Zhang, Haiyan Zhao, Guangtai Liang, Zhi Jin, and Qianxiang Wang
(Peking University, China; Huawei Technologies, China)

Certifying Graph-Manipulating C Programs via Localizations within Data Structures
Shengyi Wang, Qinxiang Cao, Anshuman Mohan, and Aquinas Hobor
(National University of Singapore, Singapore; Shanghai Jiao Tong University, China)

Duet: An Expressive Higher-Order Language and Linear Type System for Statically Enforcing Differential Privacy
Joseph P. Near, David Darais, Chike Abuah, Tim Stevens, Pranav Gaddamadugu, Lun Wang, Neel Somani, Mu Zhang, Nikhil Sharma, Alex Shan, and Dawn Song
(University of Vermont, USA; University of California at Berkeley, USA; University of Utah, USA)

Effective Lock Handling in Stateless Model Checking
Michalis Kokologiannakis, Azalea Raad, and Viktor Vafeiadis
(MPI-SWS, Germany)

FuzzFactory: Domain-Specific Fuzzing with Waypoints
Rohan Padhye, Caroline Lemieux, Koushik Sen, Laurent Simon, and Hayawardh Vijayakumar
(University of California at Berkeley, USA; Samsung Research, USA)

AL: Autogenerating Supervised Learning Programs
José P. Cambronero and Martin C. Rinard
(Massachusetts Institute of Technology, USA)

Sound and Reusable Components for Abstract Interpretation
Sven Keidel and Sebastian Erdweg
(Johannes Gutenberg University Mainz, Germany)

Design, Implementation, and Application of GPU-Based Java Bytecode Interpreters
Ahmet Celik, Pengyu Nie, Christopher J. Rossbach, and Milos Gligoric
(University of Texas at Austin, USA; VMware, USA)

Specification and Inference of Trace Refinement Relations
Timos Antonopoulos, Eric Koskinen, and Ton Chanh Le
(Yale University, USA; Stevens Institute of Technology, USA)

Dependence-Aware, Unbounded Sound Predictive Race Detection
Kaan Genç, Jake Roemer, Yufan Xu, and Michael D. Bond
(Ohio State University, USA)

Trace Aware Random Testing for Distributed Systems
Burcu Kulahcioglu Ozkan, Rupak Majumdar, and Simin Oraee
(MPI-SWS, Germany)

Coverage Guided, Property Based Testing
Leonidas Lampropoulos, Michael Hicks, and Benjamin C. Pierce
(University of Maryland, USA; University of Pennsylvania, USA)

PlanAlyzer: Assessing Threats to the Validity of Online Experiments
Emma Tosch, Eytan Bakshy, Emery D. Berger, David D. Jensen, and J. Eliot B. Moss
(University of Massachusetts Amherst, USA; Facebook, USA)

I/O Dependent Idempotence Bugs in Intermittent Systems
Milijana Surbatovich, Limin Jia, and Brandon Lucia
(Carnegie Mellon University, USA)

Initialize Once, Start Fast: Application Initialization at Build Time
Christian Wimmer, Codrut Stancu, Peter Hofer, Vojin Jovanovic, Paul Wögerer, Peter B. Kessler, Oleg Pliss, and Thomas Würthinger
(Oracle Labs, USA; Oracle Labs, Austria; Oracle Labs, Switzerland)

Safer Smart Contract Programming with Scilla
Ilya Sergey, Vaivaswatha Nagaraj, Jacob Johannsen, Amrit Kumar, Anton Trunov, and Ken Chan Guan Hao
(Yale-NUS College, Singapore; National University of Singapore, Singapore; Zilliqa Research, India; Zilliqa Research, Denmark; Zilliqa Research, UK; Zilliqa Research, Russia; Zilliqa Research, Malaysia)

ApproxHPVM: A Portable Compiler IR for Accuracy-Aware Optimizations
Hashim Sharif, Prakalp Srivastava, Muhammad Huzaifa, Maria Kotsifakou, Keyur Joshi, Yasmin Sarita, Nathan Zhao, Vikram S. Adve, Sasa Misailovic, and Sarita Adve
(University of Illinois at Urbana-Champaign, USA; Cornell University, USA)

Reflection-Aware Static Regression Test Selection
August Shi, Milica Hadzi-Tanovic, Lingming Zhang, Darko Marinov, and Owolabi Legunsen
(University of Illinois at Urbana-Champaign, USA; University of Texas at Dallas, USA)

Automatic and Scalable Detection of Logical Errors in Functional Programming Assignments
Dowon Song, Myungho Lee, and Hakjoo Oh
(Korea University, South Korea)

Detecting Nondeterministic Payment Bugs in Ethereum Smart Contracts
Shuai Wang, Chengyu Zhang, and Zhendong Su
(Hong Kong University of Science and Technology, China; East China Normal University, China; ETH Zurich, Switzerland)