OOPSLA 2024

148 papers

1. A Case for First-Class Environments · Jinhao Tan, Bruno C. d. S. Oliveira
2. A Constraint Solving Approach to Parikh Images of Regular Languages · Amanda Stjerna, Philipp Rümmer
3. A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code · Julien Simonnet, Matthieu Lemerre, Mihaela Sighireanu
4. A Learning-Based Approach to Static Program Slicing · Aashish Yadavally, Yi Li, Shaohua Wang, Tien N. Nguyen
5. A Low-Level Look at A-Normal Form · William J. Bowman
6. A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs · Vineet Rajani, Gilles Barthe, Deepak Garg
7. A Pure Demand Operational Semantics with Applications to Program Analysis · Scott F. Smith, Robert Zhang
8. A Runtime System for Interruptible Query Processing: When Incremental Computing Meets Fine-Grained Parallelism · Jeff Eymer, Philip Dexter, Joseph Raskind, Yu David Liu
9. A Typed Multi-level Datalog IR and Its Compiler Framework · David Klopp, Sebastian Erdweg, André Pacak
10. AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming · Robert Schenck, Nikolaj Hey Hinnerskov, Troels Henriksen, Magnus Madsen, Martin Elsman
11. Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning · Gabriel Ryan, Burcu Cetin, Yongwhan Lim, Suman Jana
12. AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects · Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao
13. Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models · Kartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh Jagannathan
14. Automated Verification of Parametric Channel-Based Process Communication · Georgian-Vlad Saioc, Julien Lange, Anders Møller
15. Automatically Reducing Privilege for Access Control Policies · Loris D'Antoni, Shuo Ding, Amit Goel, Mathangi Ramesh, Neha Rungta, Chungha Sung
16. Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics · Keith J. C. Johnson, Rahul Krishnan, Thomas W. Reps, Loris D'Antoni
17. Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs · Shaan Nagy, Jinwoo Kim, Thomas W. Reps, Loris D'Antoni
18. Boosting the Performance of Alias-Aware IFDS Analysis with CFL-Based Environment Transformers · Haofeng Li, Chenghang Shi, Jie Lu, Lian Li, Jingling Xue
19. CYCLE: Learning to Self-Refine the Code Generation · Yangruibo Ding, Marcus J. Min, Gail E. Kaiser, Baishakhi Ray
20. Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization · Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks + 9 more
21. Cocoon: Static Information Flow Control in Rust · Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D. Bond, Zhiqiang Lin
22. Compilation of Shape Operators on Sparse Arrays · Alexander J. Root, Bobby Yan, Peiming Liu, Christophe Gyurgyik, Aart J. C. Bik, Fredrik Kjolstad
23. Compiler Support for Sparse Tensor Convolutions · Peiming Liu, Alexander J. Root, Anlun Xu, Yinying Li, Fredrik Kjolstad, Aart J. C. Bik
24. Compiling Recurrences over Dense and Sparse Arrays · Shiv Sundram, Muhammad Usman Tariq, Fredrik Kjolstad
25. Compositionality and Observational Refinement for Linearizability with Crashes · Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You, Zhong Shao
26. Computing Precise Control Interface Specifications · Eric Hayden Campbell, Hossein Hojjat, Nate Foster
27. Concurrent Data Structures Made Easy · Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, Ilya Sergey
28. Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis · Benjamin Mariano, Ziteng Wang, Shankara Pailoor, Christian S. Collberg, Isil Dillig
29. CoolerSpace: A Language for Physically Correct and Computationally Efficient Color Programming · Ethan Chen, Jiwon Chang, Yuhao Zhu
30. Crabtree: Rust API Test Synthesis Guided by Coverage and Type · Yoshiki Takashima, Chanhee Cho, Ruben Martins, Limin Jia, Corina S. Pasareanu
31. Degrees of Separation: A Flexible Type System for Safe Concurrency · Yichen Xu, Aleksander Boruch-Gruszecki, Martin Odersky
32. Dependency-Aware Code Naturalness · Chen Yang, Junjie Chen, Jiajun Jiang, Yuliang Huang
33. Deriving Dependently-Typed OOP from First Principles · David Binder, Ingo Skupin, Tim Süberkrüb, Klaus Ostermann
34. Design and Implementation of an Aspect-Oriented C Programming Language · Zhe Chen, Yunlong Zhu, Zhemin Wang
35. Distributions for Compositionally Differentiating Parametric Discontinuities · Jesse Michel, Kevin Mu, Xuanda Yang, Sai Praveen Bangaru, Elias Rojas Collins, Gilbert Bernstein + 3 more
36. Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language Models · Ningke Li, Yuekang Li, Yi Liu, Ling Shi, Kailong Wang, Haoyu Wang
37. Effect Handlers for C via Coroutines · Mario Alvarez-Picallo, Teodoro Freund, Dan R. Ghica, Sam Lindley
38. Effects and Coeffects in Call-by-Push-Value · Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich
39. Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach · Haonan Li, Yu Hao, Yizhuo Zhai, Zhiyun Qian
40. Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks · Qian Chen, Chenyang Yu, Ruyan Liu, Chi Zhang, Yu Wang, Ke Wang + 2 more
41. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions · Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen
42. Extending the C/C++ Memory Model with Inline Assembly · Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad
43. FPCC: Detecting Floating-Point Errors via Chain Conditions · Xin Yi, Hengbiao Yu, Liqian Chen, Xiaoguang Mao, Ji Wang
44. Fast and Optimal Extraction for Sparse Equality Graphs · Amir Kafshdar Goharshady, Chun Kit Lam, Lionel Parreaux
45. Finding Cross-Rule Optimization Bugs in Datalog Engines · Chi Zhang, Linzhang Wang, Manuel Rigger
46. Finding ∀∃ Hyperbugs using Symbolic Execution · Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, Georg Weissenbacher
47. FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions · Zhengyao Lin, Joshua Gancher, Bryan Parno
48. Forge: A Tool and Language for Teaching Formal Methods · Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen + 9 more
49. Fulfilling OCaml Modules with Transparency · Clement Blaudeau, Didier Rémy, Gabriel Radanne
50. Full Iso-Recursive Types · Litao Zhou, Qianyong Wan, Bruno C. d. S. Oliveira
51. Fully Verified Instruction Scheduling · Ziteng Yang, Jun Shirako, Vivek Sarkar
52. Functional Ownership through Fractional Uniqueness · Danielle Marshall, Dominic Orchard
53. Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types · Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, Clément Pit-Claudel
54. Gradually Typed Languages Should Be Vigilant! · Olek Gierczak, Lucy Menon, Christos Dimoulas, Amal Ahmed
55. HOL4P4: Mechanized Small-Step Semantics for P4 · Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam
56. HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing · Yiyu Zhang, Tianyi Liu, Yueyang Wang, Yun Qi, Kai Ji, Jian Tang + 3 more
57. HiPy: Extracting High-Level Semantics from Python Code for Data Processing · Michael Jungmair, Alexis Engelke, Jana Giceva
58. Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification · Taro Sekiyama, Hiroshi Unno
59. Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs · Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni
60. HybridSA: GPU Acceleration of Multi-pattern Regex Matching using Bit Parallelism · Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras
61. Hydra: Generalizing Peephole Optimizations with Program Synthesis · Manasij Mukherjee, John Regehr
62. Hypra: A Deductive Program Verifier for Hyper Hoare Logic · Thibault Dardinier, Anqi Li, Peter Müller
63. Identifying and Correcting Programming Language Behavior Misconceptions · Kuang-Chen Lu, Shriram Krishnamurthi
64. Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing · Wenjia Ye, Yaozhu Sun, Bruno C. d. S. Oliveira
65. Inductive Diagrams for Causal Reasoning · Jonathan Castello, Patrick Redmond, Lindsey Kuper
66. Intensional Functions · Zachary Palmer, Nathaniel Wesley Filardo, Ke Wu
67. Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly · Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal
68. Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability · Pei Xu, Yuxiang Lei, Yulei Sui, Jingling Xue
69. Jmvx: Fast Multi-threaded Multi-version Execution and Record-Replay for Managed Languages · David Schwartz, Ankith Kowshik, Luís Pina
70. Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs · Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Anders Freeman, Carolyn Jane Anderson + 4 more
71. Law and Order for Typestate with Borrowing · Hannes Saffrich, Yuki Nishida, Peter Thiemann
72. Learning Abstraction Selection for Bayesian Program Analysis · Yifan Zhang, Yuanfeng Shi, Xin Zhang
73. Lexical Effect Handlers, Directly · Cong Ma, Zhaoyi Ge, Edward Lee, Yizhou Zhang
74. MEA2: A Lightweight Field-Sensitive Escape Analysis with Points-to Calculation for Golang · Boyao Ding, Qingwei Li, Yu Zhang, Fugen Tang, Jinbao Chen
75. Making Formulog Fast: An Argument for Unconventional Datalog Evaluation · Aaron Bembenek, Michael Greenberg, Stephen Chong
76. Making Sense of Multi-threaded Application Performance at Scale with NonSequitur · Augustine Wong, Paul Bucci, Ivan Beschastnikh, Alexandra Fedorova
77. Mark-Scavenge: Waiting for Trash to Take Itself Out · Jonas Norlinder, Erik Österlund, David Black-Schaffer, Tobias Wrigstad
78. Mechanizing the CMP Abstraction for Parameterized Verification · Yongjian Li, Bohua Zhan, Jun Pang
79. Merging Gradual Typing · Wenjia Ye, Bruno C. d. S. Oliveira, Matías Toro
80. Message-Observing Sessions · Ryan Kavanagh, Brigitte Pientka
81. Minotaur: A SIMD-Oriented Synthesizing Superoptimizer · Zhengyang Liu, Stefan Mada, John Regehr
82. Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations · Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen + 1 more
83. Model Checking Distributed Protocols in Must · Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, Rupak Majumdar
84. Modeling Dynamic (De)Allocations of Local Memory for Translation Validation · Abhishek Rose, Sorav Bansal
85. Modular Synthesis of Efficient Quantum Uncomputation · Hristo Venev, Timon Gehr, Dimitar Dimitrov, Martin T. Vechev
86. Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials · Nikhil Pimpalkhare, Zachary Kincaid
87. Multiverse Notebook: Shifting Data Scientists to Time Travelers · Shigeyuki Sato, Tomoki Nakamaru
88. Multris: Functional Verification of Multiparty Message Passing in Separation Logic · Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers
89. Newtonian Program Analysis of Probabilistic Programs · Di Wang, Thomas W. Reps
90. Non-termination Proving at Scale · Azalea Raad, Julien Vanegue, Peter W. O'Hearn
91. Object-Oriented Fixpoint Programming with Datalog · David Klopp, Sebastian Erdweg, André Pacak
92. On the Expressive Power of Languages for Static Variability · Paul Maximilian Bittner, Alexander Schultheiß, Benjamin Moosherr, Jeffrey M. Young, Leopoldo Teixeira, Eric Walkingshaw + 2 more
93. Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects · Noam Zilberstein, Angelina Saliling, Alexandra Silva
94. PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis · Zhaoyu Wang, Pingchuan Ma, Huaijin Wang, Shuai Wang
95. PROMPT: A Fast and Extensible Memory Profiling Framework · Ziyang Xu, Yebin Chon, Yian Su, Zujun Tan, Sotiris Apostolakis, Simone Campanoni + 1 more
96. ParDiff: Practical Static Differential Analysis of Network Protocol Parsers · Mingwei Zheng, Qingkai Shi, Xuwei Liu, Xiangzhe Xu, Le Yu, Congyu Liu + 2 more
97. Persimmon: Nested Family Polymorphism with Extensible Variant Types · Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, Nada Amin
98. Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels · Si Liu, Long Gu, Hengfeng Wei, David A. Basin
99. PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting · Chijin Zhou, Bingzhou Qian, Gwihwan Go, Quan Zhang, Shanshan Li, Yu Jiang
100. Practical Verification of Smart Contracts using Memory Splitting · Shelly Grossman, John Toman, Alexander Bakst, Sameer Arora, Mooly Sagiv, Chandrakana Nandi
101. Profiling Programming Language Learning · Will Crichton, Shriram Krishnamurthi
102. Programmable MCMC with Soundly Composed Guide Programs · Long Pham, Di Wang, Feras A. Saad, Jan Hoffmann
103. PyDex: Repairing Bugs in Introductory Python Assignments using LLMs · Jialu Zhang, José Pablo Cambronero, Sumit Gulwani, Vu Le, Ruzica Piskac, Gustavo Soares + 1 more
104. QuAC: Quick Attribute-Centric Type Inference for Python · Jifeng Wu, Caroline Lemieux
105. Qualifying System F<: Some Terms and Conditions May Apply · Edward Lee, Yaoyu Zhao, Ondrej Lhoták, James You, Kavin Satheeskumar, Jonathan Immanuel Brachthäuser
106. Quantitative Bounds on Resource Usage of Probabilistic Programs · Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde Zikelic
107. Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers · Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, Alexandra Silva
108. Quantum Control Machine: The Limits of Control Flow in Quantum Programming · Charles Yuan, Agnes Villanyi, Michael Carbin
109. Quantum Probabilistic Model Checking for Time-Bounded Properties · Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, Jeehoon Kang
110. Quarl: A Learning-Based Quantum Circuit Optimizer · Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon + 1 more
111. Realistic Realizability: Specifying ABIs You Can Count On · Andrew Wagner, Zachary Eisbach, Amal Ahmed
112. Refinement Type Refutations · Robin Webbers, Klaus von Gleissenthall, Ranjit Jhala
113. Reward Augmentation in Reinforcement Learning for Testing Distributed Systems · Andrea Borgarelli, Constantin Enea, Rupak Majumdar, Srinidhi Nagendra
114. Rustlantis: Randomized Differential Testing of the Rust Compiler · Qian Wang, Ralf Jung
115. SMT2Test: From SMT Formulas to Effective Test Cases · Chengyu Zhang, Zhendong Su
116. Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks · Zhenyu Yan, Xin Zhang, Peng Di
117. Scenario-Based Proofs for Concurrent Objects · Constantin Enea, Eric Koskinen
118. Semantic-Type-Guided Bug Finding · Kelvin Qian, Scott F. Smith, Brandon Stride, Shiwei Weng, Ke Wu
119. Semantics Lifting for Syntactic Sugar · Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, Zhenjiang Hu
120. Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures · Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad
121. Seneca: Taint-Based Call Graph Construction for Java Object Deserialization · Joanna C. S. Santos, Mehdi Mirakhorli, Ali Shokri
122. Sensitivity by Parametricity · Elisabet Lobo Vesga, Alejandro Russo, Marco Gaboardi, Carlos Tomé Cortiñas
123. Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs · Dennis Liew, Tiago Cogumbreiro, Julien Lange
124. SparseAuto: An Auto-scheduler for Sparse Tensor Computations using Recursive Loop Nest Restructuring · Adhitha Dias, Logan Anderson, Kirshanthan Sundararajah, Artem Pelenitsyn, Milind Kulkarni
125. StarMalloc: Verifying a Modern, Hardened Memory Allocator · Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko
126. Statically Contextualizing Large Language Models with Typed Holes · Andrew Blinn, Xiang Li, June Hyung Kim, Cyrus Omar
127. Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification · Chan Gu Kang, Joonghoon Lee, Hakjoo Oh
128. Synthesizing Formal Semantics from Executable Interpreters · Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith J. C. Johnson, Thomas W. Reps, Loris D'Antoni
129. Synthetiq: Fast and Versatile Quantum Circuit Synthesis · Anouk Paradis, Jasper Dekoninck, Benjamin Bichsel, Martin T. Vechev
130. Tachis: Higher-Order Separation Logic with Credits for Expected Costs · Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti + 1 more
131. Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation · Qianchuan Ye, Benjamin Delaware
132. The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and Efficiently · Shashin Halalingaiah, Vijay Sundaresan, Daryl Maier, V. Krishna Nandivada
133. The Ultimate Conditional Syntax · Luyu Cheng, Lionel Parreaux
134. TorchQL: A Programming Framework for Integrity Constraints in Machine Learning · Aaditya Naik, Adam Stein, Yinjun Wu, Mayur Naik, Eric Wong
135. Type Inference Logics · Denis Carnier, François Pottier, Steven Keuchel
136. Understanding and Finding Java Decompiler Bugs · Yifei Lu, Weidong Hou, Minxue Pan, Xuandong Li, Zhendong Su
137. UniSparse: An Intermediate Language for General Sparse Format Customization · Jie Liu, Zhongyuan Zhao, Zijian Ding, Benjamin Brock, Hongbo Rong, Zhiru Zhang
138. Unifying Static and Dynamic Intermediate Languages for Accelerator Generators · Caleb Kim, Pai Li, Anshuman Mohan, Andrew Butt, Adrian Sampson, Rachit Nigam
139. Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration · Dominik Winterer, Zhendong Su
140. VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts · Yichuan Li, Wei Song, Jeff Huang
141. VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints · Yang He, Pinhan Zhao, Xinyu Wang, Yuepeng Wang
142. Verification of Neural Networks' Global Robustness · Anan Kabaha, Dana Drachsler-Cohen
143. Verified Lock-Free Session Channels with Linking · Thomas Somers, Robbert Krebbers
144. Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks · Doehyun Baek, Jakob Getz, Yusung Sim, Daniel Lehmann, Ben L. Titzer, Sukyoung Ryu + 1 more
145. Weighted Context-Free-Language Ordered Binary Decision Diagrams · Meghana Sistla, Swarat Chaudhuri, Thomas W. Reps
146. When Your Infrastructure Is a Buggy Program: Understanding Faults in Infrastructure as Code Ecosystems · Georgios-Petros Drosos, Thodoris Sotiropoulos, Georgios Alexopoulos, Dimitris Mitropoulos, Zhendong Su
147. WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models · Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand + 1 more
148. libLISA: Instruction Discovery and Analysis on x86-64 · Jos Craaijo, Freek Verbeek, Binoy Ravindran