Venues / OOPSLA /

OOPSLA 2023

110 papers

A Cocktail Approach to Practical Call Graph Construction · Yuandao Cai, Charles Zhang
A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis · Dongjie He, Yujiang Gui, Wei Li, Yonggang Tao, Changwei Zou, Yulei Sui + 1 more
A Deductive Verification Infrastructure for Probabilistic Programs · Philipp Schröer, Kevin Batz, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Christoph Matheja
A Gradual Probabilistic Lambda Calculus · Wenjia Ye, Matías Toro, Federico Olmedo
A Grounded Conceptual Model for Ownership Types in Rust · Will Crichton, Gavin Gray, Shriram Krishnamurthi
A Pretty Expressive Printer · Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations · Anthony C. J. Fox, Gareth Stockwell, Shale Xiong, Hanno Becker, Dominic P. Mulligan, Gustavo Petri + 1 more
AST vs. Bytecode: Interpreters in the Age of Meta-Compilation · Octave Larose, Sophie Kaleba, Humphrey Burchell, Stefan Marr
Accelerating Fuzzing through Prefix-Guided Execution · Shaohua Li, Zhendong Su
Adventure of a Lifetime: Extract Method Refactoring for Rust · Sewen Thy, Andreea Costea, Kiran Gopinathan, Ilya Sergey
Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs · Amir Kafshdar Goharshady, S. Hitarth, Fatemeh Mohammadi, Harshit J. Motwani
Aliasing Limits on Translating C to Safe Rust · Mehmet Emre, Peter Boyland, Aesha Parekh, Ryan Schroeder, Kyle Dewey, Ben Hardekopf
An Explanation Method for Models of Code · Yu Wang, Ke Wang, Linzhang Wang
Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts · Zhuo Cai, Soroush Farokhnia, Amir Kafshdar Goharshady, S. Hitarth
AtomiS: Data-Centric Synchronization Made Practical · Hervé Paulino, Ana Almeida Matos, Jan Cederquist, Marco Giunti, João Matos, António Ravara
Automated Ambiguity Detection in Layout-Sensitive Grammars · Jiangyi Liu, Fengmin Zhu, Fei He
Automated Translation of Functional Big Data Queries to SQL · Guoqiang Zhang, Benjamin Mariano, Xipeng Shen, Isil Dillig
Back to Direct Style: Typed and Tight · Marius Müller, Philipp Schuster, Jonathan Immanuel Brachthäuser, Klaus Ostermann
Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics · Girish Mururu, Sharjeel Khan, Bodhisatwa Chatterjee, Chao Chen, Chris Porter, Ada Gavrilovska + 1 more
Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects · Xing Zhang, Guanchen Guo, Xiao He, Zhenjiang Hu
Bring Your Own Data Structures to Datalog · Arash Sahebolamri, Langston Barrett, Scott Moore, Kristopher K. Micinski
Building Dynamic System Call Sandbox with Partial Order Analysis · Quan Zhang, Chijin Zhou, Yiwen Xu, Zijing Yin, Mingzhe Wang, Zhuo Su + 3 more
Compiling Structured Tensor Algebra · Mahdi Ghorbani, Mathieu Huot, Shideh Hashemian, Amir Shaikhha
Complete First-Order Reasoning for Properties of Functional Programs · Adithya Murali, Lucas Peña, Ranjit Jhala, P. Madhusudan
Compositional Security Definitions for Higher-Order Where Declassification · Jan Menz, Andrew K. Hirsch, Peixuan Li, Deepak Garg
Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks · Pengfei Gao, Yedi Zhang, Fu Song, Taolue Chen, François-Xavier Standaert
Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving · Fangke Ye, Jisheng Zhao, Jun Shirako, Vivek Sarkar
Continuing WebAssembly with Effect Handlers · Luna Phipps-Costin, Andreas Rossberg, Arjun Guha, Daan Leijen, Daniel Hillerström, K. C. Sivaramakrishnan + 2 more
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols · Orr Tamir, Marcelo Taube, Kenneth L. McMillan, Sharon Shoham, Jon Howell, Guy Gueta + 1 more
Data Extraction via Semantic Regular Expression Synthesis · Qiaochu Chen, Arko Banerjee, Çagatay Demiralp, Greg Durrett, Isil Dillig
Deep Learning Robustness Verification for Few-Pixel Attacks · Yuval Shapira, Eran Avneri, Dana Drachsler-Cohen
Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions · Christopher Wagner, Nouraldin Jaber, Roopsha Samanta
Equality Saturation Theory Exploration à la Carte · Anjali Pal, Brett Saiki, Ryan Tjoa, Cynthia Richey, Amy Zhu, Oliver Flatt + 3 more
Exact Recursive Probabilistic Programming · David Chiang, Colin McDonald, Chung-chieh Shan
Explainable Program Synthesis by Localizing Specifications · Amirmohammad Nazari, Yifei Huang, Roopsha Samanta, Arjun Radhakrishna, Mukund Raghothaman
Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis · Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Kerim Kochekov, Yun Chen Tsai, Ahmed Khaled Zaher
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems · Magnus Madsen, Jaco van de Pol, Troels Henriksen
Fat Pointers for Temporal Memory Safety of C · Jie Zhou, John Criswell, Michael Hicks
Fluent APIs in Functional Languages · Ori Roth, Yossi Gil
Formal Abstractions for Packet Scheduling · Anshuman Mohan, Yunhe Liu, Nate Foster, Tobias Kappé, Dexter Kozen
Formally Verifying Optimizations with Block Simulations · Léo Gourdin, Benjamin Bonneau, Sylvain Boulmé, David Monniaux, Alexandre Bérard
From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers · Marius Müller, Philipp Schuster, Jonathan Lindegaard Starup, Klaus Ostermann, Jonathan Immanuel Brachthäuser
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier · Zhengyao Lin, Xiaohong Chen, Minh-Thai Trinh, John Wang, Grigore Rosu
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference · Ishan Bhanuka, Lionel Parreaux, David Binder, Jonathan Immanuel Brachthäuser
Gradual Typing for Effect Handlers · Max S. New, Eric Giovannini, Daniel R. Licata
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies · Oliver Bracevac, Guannan Wei, Songlin Jia, Supun Abeysinghe, Yuxuan Jiang, Yuyan Bao + 1 more
Greedy Implicit Bounded Quantification · Chen Cui, Shengyi Jiang, Bruno C. d. S. Oliveira
Grounded Copilot: How Programmers Interact with Code-Generating Models · Shraddha Barke, Michael B. James, Nadia Polikarpova
Hardware-Aware Static Optimization of Hyperdimensional Computations · Pu (Luke) Yi, Sara Achour
Historia: Refuting Callback Reachability with Message-History Logics · Shawn Meier, Sergio Mover, Gowtham Kaki, Bor-Yuh Evan Chang
How Domain Experts Use an Embedded DSL · Lisa Rennels, Sarah E. Chasins
How Profilers Can Help Navigate Type Migration · Ben Greenman, Matthias Felleisen, Christos Dimoulas
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection · Lorenzo Gheri, Nobuko Yoshida
Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection · Ruyi Ji, Chaozhe Kong, Yingfei Xiong, Zhenjiang Hu
Inductive Program Synthesis Guided by Observational Program Similarity · John K. Feser, Isil Dillig, Armando Solar-Lezama
Inference of Resource Management Specifications · Narges Shadab, Pritam M. Gharat, Shrey Tiwari, Michael D. Ernst, Martin Kellogg, Shuvendu K. Lahiri + 2 more
Initializing Global Objects: Time and Order · Fengyun Liu, Ondrej Lhoták, David Hua, Enze Xing
Interactive Debugging of Datalog Programs · André Pacak, Sebastian Erdweg
Languages with Decidable Learning: A Meta-theorem · Paul Krogmeier, P. Madhusudan
Leaf: Modularity for Temporary Sharing in Separation Logic · Travis Hance, Jon Howell, Oded Padon, Bryan Parno
Live Pattern Matching with Typed Holes · Yongwei Yuan, Scott Guest, Eric Griffis, Hannah Potter, David Moon, Cyrus Omar
Lower Bounds for Possibly Divergent Probabilistic Programs · Shenghua Feng, Mingshuai Chen, Han Su, Benjamin Lucien Kaminski, Joost-Pieter Katoen, Naijun Zhan
Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid · Huanqi Cao, Shizhi Tang, Qianchao Zhu, Bowen Yu, Wenguang Chen
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity · Chuta Sano, Ryan Kavanagh, Brigitte Pientka
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C · Armaël Guéneau, Johannes Hostert, Simon Spies, Michael Sammler, Lars Birkedal, Derek Dreyer
MemPerf: Profiling Allocator-Induced Performance Slowdowns · Jin Zhou, Sam Silvestro, Steven (Jiaxun) Tang, Hanmei Yang, Hongyu Liu, Guangming Zeng + 3 more
Message Chains for Distributed System Verification · Federico Mora, Ankush Desai, Elizabeth Polgreen, Sanjit A. Seshia
Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates · Aalok Thakkar, Nathaniel Sands, George Petrou, Rajeev Alur, Mayur Naik, Mukund Raghothaman
Modular Component-Based Quantum Circuit Synthesis · Chan Gu Kang, Hakjoo Oh
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic · Jaehwang Jung, Janggun Lee, Jaemin Choi, Jaewoo Kim, Sunho Park, Jeehoon Kang
Mutually Iso-Recursive Subtyping · Andreas Rossberg
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning · Noam Zilberstein, Derek Dreyer, Alexandra Silva
P4R-Type: A Verified API for P4 Control Plane Programs · Jens Kanstrup Larsen, Roberto Guanciale, Philipp Haller, Alceste Scalas
Perception Contracts for Safety of ML-Enabled Systems · Angello Astorga, Chiao Hsieh, P. Madhusudan, Sayan Mitra
Proof Automation for Linearizability in Separation Logic · Ike Mulder, Robbert Krebbers
Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction · Zhenyang Xu, Yongqiang Tian, Mengxiao Zhang, Gaosen Zhao, Yu Jiang, Chengnian Sun
Quantifying and Mitigating Cache Side Channel Leakage with Differential Set · Cong Ma, Dinghao Wu, Gang Tan, Mahmut Taylan Kandemir, Danfeng Zhang
Randomized Testing of Byzantine Fault Tolerant Algorithms · Levin N. Winter, Florena Buse, Daan de Graaf, Klaus von Gleissenthall, Burcu Kulahcioglu Ozkan
Rapid: Region-Based Pointer Disambiguation · Khushboo Chitre, Piyus Kedia, Rahul Purandare
Reference Capabilities for Flexible Memory Management · Ellen Arvidsson, Elias Castegren, Sylvan Clebsch, Sophia Drossopoulou, James Noble, Matthew J. Parkinson + 1 more
Regular Expression Matching using Bit Vector Automata · Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras
Resource-Aware Soundness for Big-Step Semantics · Riccardo Bianchini, Francesco Dagnino, Paola Giannini, Elena Zucca
Reusing Just-in-Time Compiled Code · Meetesh Kalpesh Mehta, Sebastián Krynski, Hugo Musso Gualandi, Manas Thakur, Jan Vitek
Rhombus: A New Spin on Macros without All the Parentheses · Matthew Flatt, Taylor Allred, Nia Angle, Stephen De Gabrielle, Robert Bruce Findler, Jack Firth + 9 more
Run-Time Prevention of Software Integration Failures of Machine Learning APIs · Chengcheng Wan, Yuhan Liu, Kuntai Du, Henry Hoffmann, Junchen Jiang, Michael Maire + 1 more
Saggitarius: A DSL for Specifying Grammatical Domains · Anders Miltner, Devon Loehr, Arnold Mong, Kathleen Fisher, David Walker
Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data · Thierry Renaux, Sam Van den Vonder, Wolfgang De Meuter
Simple Reference Immutability for System F · Edward Lee, Ondrej Lhoták
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case · Chenglin Wang, Fangzhen Lin
Solving String Constraints with Lengths by Stabilization · Yu-Fang Chen, David Chocholatý, Vojtech Havlena, Lukás Holík, Ondrej Lengál, Juraj Síc
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory · Simon Friis Vindum, Lars Birkedal
Static Analysis of Memory Models for SMT Encodings · Thomas Haas, René Pascasl Maseli, Roland Meyer, Hernán Ponce de León
Structural Subtyping as Parametric Polymorphism · Wenhao Tang, Daniel Hillerström, James McKinna, Michel Steuwer, Ornela Dardha, Rongxiao Fu + 1 more
Stuttering for Free · Minki Cho, Youngju Song, Dongjae Lee, Lennard Gäher, Derek Dreyer
Synthesizing Efficient Memoization Algorithms · Yican Sun, Xuanyu Peng, Yingfei Xiong
Synthesizing Precise Static Analyzers for Automatic Differentiation · Jacob Laurel, Siyuan Brant Qian, Gagandeep Singh, Sasa Misailovic
Synthesizing Specifications · Kanghee Park, Loris D'Antoni, Thomas W. Reps
TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism · Matt D'Souza, James You, Ondrej Lhoták, Aleksandar Prokopec
The Bounded Pathwidth of Control-Flow Graphs · Giovanna Kobus Conrado, Amir Kafshdar Goharshady, Chun Kit Lam
The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog · Qinlin Chen, Nairen Zhang, Jinpeng Wang, Tian Tan, Chang Xu, Xiaoxing Ma + 1 more
Towards Better Semantics Exploration for Browser Fuzzing · Chijin Zhou, Quan Zhang, Lihua Guo, Mingzhe Wang, Yu Jiang, Qing Liao + 3 more
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs · Alex Renda, Yi Ding, Michael Carbin
Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network · Shangwen Wang, Bo Lin, Zhensu Sun, Ming Wen, Yepang Liu, Yan Lei + 1 more
Type-Safe Dynamic Placement with First-Class Placed Values · George Zakhour, Pascal Weisenburger, Guido Salvaneschi
User-Customizable Transpilation of Scripting Languages · Bo Wang, Aashish Kolluri, Ivica Nikolic, Teodora Baluta, Prateek Saxena
Validating IoT Devices with Rate-Based Session Types · Grant Iraci, Cheng-En Chuang, Raymond Hu, Lukasz Ziarek
Verification-Preserving Inlining in Automatic Separation Logic Verifiers · Thibault Dardinier, Gaurav Parthasarathy, Peter Müller
Verifying Indistinguishability of Privacy-Preserving Protocols · Kirby Linvill, Gowtham Kaki, Eric Wustrow
Verus: Verifying Rust Programs using Linear Ghost Types · Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou + 3 more
When Concurrency Matters: Behaviour-Oriented Concurrency · Luke Cheeseman, Matthew J. Parkinson, Sylvan Clebsch, Marios Kogias, Sophia Drossopoulou, David Chisnall + 2 more