PLDI 2024
Proceedings of the ACM on Programming Languages, Volume 8, Number PLDI
Powered by
Conference Publishing Consulting

Proceedings of the ACM on Programming Languages, Volume 8, Number PLDI, June 24–28, 2024, Copenhagen, Denmark

PLDI – Journal Issue

Contents - Abstracts - Authors

Frontmatter

Title Page
Editorial Message
Sponsors

Papers

Input-Relational Verification of Deep Neural Networks
Debangshu Banerjee ORCID logo, Changming Xu ORCID logo, and Gagandeep SinghORCID logo
(University of Illinois at Urbana-Champaign, USA; VMware Research, USA)
Preprint Info Artifacts Available Artifacts Reusable
Modular Hardware Design of Pipelined Circuits with Hazards
Minseong Jang ORCID logo, Jungin Rhee ORCID logo, Woojin Lee ORCID logo, Shuangshuang Zhao ORCID logo, and Jeehoon KangORCID logo
(KAIST, South Korea)
Article Search Info Artifacts Available Artifacts Reusable
Verified Extraction from Coq to OCaml
Yannick Forster ORCID logo, Matthieu Sozeau ORCID logo, and Nicolas TabareauORCID logo
(Inria, France)
Article Search
Robust Resource Bounds with Static Analysis and Bayesian Inference
Long Pham ORCID logo, Feras A. SaadORCID logo, and Jan Hoffmann ORCID logo
(Carnegie Mellon University, USA)
Article Search Archive submitted (4.3 MB) Artifacts Available Artifacts Reusable
Recursive Program Synthesis using Paramorphisms
Qiantan Hong ORCID logo and Alex Aiken ORCID logo
(Stanford University, USA)
Article Search
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption
Aleksandar Krastev ORCID logo, Nikola Samardzic ORCID logo, Simon Langowski ORCID logo, Srinivas Devadas ORCID logo, and Daniel Sanchez ORCID logo
(Massachusetts Institute of Technology, USA)
Article Search
Concurrent Immediate Reference Counting
Jaehwang Jung ORCID logo, Jeonghyeon Kim ORCID logo, Matthew J. Parkinson ORCID logo, and Jeehoon KangORCID logo
(KAIST, South Korea; Microsoft Azure, United Kingdom)
Article Search Artifacts Available Artifacts Reusable
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic
Sunho Park ORCID logo, Jaewoo Kim ORCID logo, Ike MulderORCID logo, Jaehwang Jung ORCID logo, Janggun Lee ORCID logo, Robbert KrebbersORCID logo, and Jeehoon KangORCID logo
(KAIST, South Korea; Radboud University Nijmegen, Netherlands)
Article Search Artifacts Available Artifacts Reusable
Diffy: Data-Driven Bug Finding for Configurations
Siva Kesava Reddy KakarlaORCID logo, Francis Y. Yan ORCID logo, and Ryan Beckett ORCID logo
(Microsoft Research, USA)
Article Search Archive submitted (850 kB) Artifacts Available
Boosting Compiler Testing by Injecting Real-World Code
Shaohua Li ORCID logo, Theodoros Theodoridis ORCID logo, and Zhendong Su ORCID logo
(ETH Zurich, Switzerland)
Article Search Artifacts Reusable
SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories
Benjamin Mikek ORCID logo and Qirun Zhang ORCID logo
(Georgia Institute of Technology, USA)
Article Search Artifacts Available Artifacts Reusable
Compilation of Qubit Circuits to Optimized Qutrit Circuits
Ritvik Sharma ORCID logo and Sara Achour ORCID logo
(Stanford University, USA)
Article Search Archive submitted (260 kB) Artifacts Available Artifacts Reusable
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes
Aditya AnandORCID logo, Solai Adithya ORCID logo, Swapnil Rustagi ORCID logo, Priyam Seth ORCID logo, Vijay Sundaresan ORCID logo, Daryl Maier ORCID logo, V. Krishna Nandivada ORCID logo, and Manas Thakur ORCID logo
(IIT Bombay, India; IIT Mandi, India; IBM, Canada; IIT Madras, India)
Preprint Artifacts Available Artifacts Functional
A Verified Compiler for a Functional Tensor Language
Amanda Liu ORCID logo, Gilbert Bernstein ORCID logo, Adam ChlipalaORCID logo, and Jonathan Ragan-Kelley ORCID logo
(Massachusetts Institute of Technology, USA; University of Washington, USA)
Article Search Archive submitted (330 kB) Artifacts Available Artifacts Reusable
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications
Chujun Geng ORCID logo, Spyros Blanas ORCID logo, Michael D. Bond ORCID logo, and Yang Wang ORCID logo
(Ohio State University, USA)
Article Search Artifacts Available Artifacts Reusable
Compiling with Abstract Interpretation
Dorian LesbreORCID logo and Matthieu Lemerre ORCID logo
(CEA LIST, France)
Article Search Artifacts Available Artifacts Reusable
Associated Effects: Flexible Abstractions for Effectful Programming
Matthew Lutze ORCID logo and Magnus Madsen ORCID logo
(Aarhus University, Denmark)
Article Search Artifacts Available Artifacts Reusable
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs
Mafalda Ferreira ORCID logo, Miguel Monteiro ORCID logo, Tiago Brito ORCID logo, Miguel E. Coimbra ORCID logo, Nuno Santos ORCID logo, Limin Jia ORCID logo, and José Fragoso Santos ORCID logo
(INESC-ID, Portugal; Universidade de Lisboa, Portugal; Carnegie Mellon University, USA)
Article Search Artifacts Available Artifacts Reusable
Floating-Point TVPI Abstract Domain
Joao Rivera ORCID logo, Franz Franchetti ORCID logo, and Markus Püschel ORCID logo
(ETH Zurich, Switzerland; Carnegie Mellon University, USA)
Article Search Archive submitted (490 kB) Artifacts Available Artifacts Reusable
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks
Ajay BrahmakshatriyaORCID logo, Chris Rinard ORCID logo, Manya Ghobadi ORCID logo, and Saman AmarasingheORCID logo
(Massachusetts Institute of Technology, USA)
Article Search Artifacts Reusable
The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation
Charles Yuan ORCID logo and Michael CarbinORCID logo
(Massachusetts Institute of Technology, USA)
Preprint Archive submitted (520 kB) Artifacts Available Artifacts Reusable
The Functional Essence of Imperative Binary Search Trees
Anton Lorenzen ORCID logo, Daan LeijenORCID logo, Wouter SwierstraORCID logo, and Sam Lindley ORCID logo
(University of Edinburgh, United Kingdom; Microsoft Research, Redmond, USA; Utrecht University, Netherlands)
Article Search Artifacts Available Artifacts Reusable
Compositional Semantics for Shared-Variable Concurrency
Mikhail Svyatlovskiy ORCID logo, Shai Mermelstein ORCID logo, and Ori LahavORCID logo
(Tel Aviv University, Israel)
Article Search Artifacts Available Artifacts Reusable
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis
Peisen Yao ORCID logo, Jinguo Zhou ORCID logo, Xiao Xiao ORCID logo, Qingkai Shi ORCID logo, Rongxin Wu ORCID logo, and Charles ZhangORCID logo
(Zhejiang University, China; Ant Group, China; Nanjing University, China; Xiamen University, China; Hong Kong University of Science and Technology, China)
Article Search
Allo: A Programming Model for Composable Accelerator Design
Hongzheng Chen ORCID logo, Niansong Zhang ORCID logo, Shaojie Xiang ORCID logo, Zhichen Zeng ORCID logo, Mengjia Dai ORCID logo, and Zhiru Zhang ORCID logo
(Cornell University, USA; University of Science and Technology of China, China)
Preprint Archive submitted (870 kB) Artifacts Available Artifacts Reusable
VESTA: Power Modeling with Language Runtime Events
Joseph Raskind ORCID logo, Timur Babakol ORCID logo, Khaled Mahmoud ORCID logo, and Yu David LiuORCID logo
(SUNY Binghamton, USA)
Article Search Artifacts Reusable
Mechanised Hypersafety Proofs about Structured Data
Vladimir GladshteinORCID logo, Qiyuan ZhaoORCID logo, Willow AhrensORCID logo, Saman AmarasingheORCID logo, and Ilya SergeyORCID logo
(National University of Singapore, Singapore; Massachusetts Institute of Technology, USA)
Article Search Artifacts Available Artifacts Reusable
Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior
Theodoros Theodoridis ORCID logo and Zhendong Su ORCID logo
(ETH Zurich, Switzerland)
Article Search Artifacts Available Artifacts Reusable
Jacdac: Service-Based Prototyping of Embedded Systems
Thomas Ball ORCID logo, Peli de Halleux ORCID logo, James Devine ORCID logo, Steve Hodges ORCID logo, and Michał Moskal ORCID logo
(Microsoft, USA; Microsoft, United Kingdom; Lancaster University, United Kingdom)
Article Search Artifacts Available Artifacts Reusable
Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation
Jaemin Hong ORCID logo and Sukyoung RyuORCID logo
(KAIST, South Korea)
Article Search Artifacts Reusable
Quantitative Robustness for Vulnerability Assessment
Guillaume Girol ORCID logo, Guilhem Lacombe ORCID logo, and Sébastien BardinORCID logo
(CEA LIST, France; Université Paris-Saclay, France)
Article Search Archive submitted (540 kB) Artifacts Reusable
Automated Verification of Fundamental Algebraic Laws
George Zakhour ORCID logo, Pascal Weisenburger ORCID logo, and Guido SalvaneschiORCID logo
(University of St. Gallen, Switzerland)
Preprint Info Artifacts Available Artifacts Reusable
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables
Mathieu Huot ORCID logo, Matin Ghavami ORCID logo, Alexander K. LewORCID logo, Ulrich Schaechtle ORCID logo, Cameron E. Freer ORCID logo, Zane Shelby ORCID logo, Martin C. RinardORCID logo, Feras A. SaadORCID logo, and Vikash K. MansinghkaORCID logo
(Massachusetts Institute of Technology, USA; Digital Garage, Japan; Carnegie Mellon University, USA)
Article Search Artifacts Available Artifacts Reusable
Daedalus: Safer Document Parsing
Iavor S. Diatchki ORCID logo, Mike Dodds ORCID logo, Harrison GoldsteinORCID logo, Bill Harris ORCID logo, David A. Holland ORCID logo, Benoit Razet ORCID logo, Cole Schlesinger ORCID logo, and Simon Winwood ORCID logo
(Galois, USA; University of Pennsylvania, USA)
Article Search Artifacts Available Artifacts Reusable
Descend: A Safe GPU Systems Programming Language
Bastian Köpcke ORCID logo, Sergei Gorlatch ORCID logo, and Michel Steuwer ORCID logo
(University of Münster, Germany; TU Berlin, Germany)
Article Search
Bit Blasting Probabilistic Programs
Poorva Garg ORCID logo, Steven Holtzen ORCID logo, Guy Van den BroeckORCID logo, and Todd Millstein ORCID logo
(University of California at Los Angeles, Los Angeles, USA; Northeastern University, USA)
Preprint Artifacts Available Artifacts Functional
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq
Simon Spies ORCID logo, Lennard Gäher ORCID logo, Michael Sammler ORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany)
Article Search Artifacts Available Artifacts Reusable
Program Analysis for Adaptive Data Analysis
Jiawen Liu ORCID logo, Weihao QuORCID logo, Marco Gaboardi ORCID logo, Deepak GargORCID logo, and Jonathan Ullman ORCID logo
(Boston University, USA; Monmouth University, USA; MPI-SWS, Germany; Northeastern University, USA)
Article Search Info Artifacts Available Artifacts Reusable
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
Ruyi Ji ORCID logo, Yuwei Zhao ORCID logo, Nadia Polikarpova ORCID logo, Yingfei Xiong ORCID logo, and Zhenjiang Hu ORCID logo
(Peking University, China; University of California at San Diego, USA)
Article Search Artifacts Available Artifacts Reusable
Consolidating Smart Contracts with Behavioral Contracts
Guannan Wei ORCID logo, Danning XieORCID logo, Wuqi Zhang ORCID logo, Yongwei Yuan ORCID logo, and Zhuo Zhang ORCID logo
(Purdue University, USA; Hong Kong University of Science and Technology, China)
Article Search
Scaling Type-Based Points-to Analysis with Saturation
Christian Wimmer ORCID logo, Codrut Stancu ORCID logo, David Kozak ORCID logo, and Thomas Würthinger ORCID logo
(Oracle Labs, USA; Oracle Labs, Switzerland; Brno University of Technology, Czechia; Oracle Labs, Czechia)
Article Search Artifacts Reusable
From Batch to Stream: Automatic Generation of Online Algorithms
Ziteng Wang ORCID logo, Shankara Pailoor ORCID logo, Aaryan Prakash ORCID logo, Yuepeng Wang ORCID logo, and Işıl Dillig ORCID logo
(University of Texas at Austin, USA; Simon Fraser University, Canada)
Article Search Artifacts Available Artifacts Reusable
Symbolic Execution for Quantum Error Correction Programs
Wang Fang ORCID logo and Mingsheng Ying ORCID logo
(Institute of Software at Chinese Academy of Sciences, Beijing, China; University of Chinese Academy of Sciences, China; Tsinghua University, China)
Preprint Artifacts Available Artifacts Reusable
Wavefront Threading Enables Effective High-Level Synthesis
Blake Pelton ORCID logo, Adam Sapek ORCID logo, Ken Eguro ORCID logo, Daniel Lo ORCID logo, Alessandro Forin ORCID logo, Matt Humphrey ORCID logo, Jinwen Xi ORCID logo, David Cox ORCID logo, Rajas Karandikar ORCID logo, Johannes de Fine Licht ORCID logo, Evgeny Babin ORCID logo, Adrian Caulfield ORCID logo, and Doug Burger ORCID logo
(Microsoft, USA; ETH Zurich, Switzerland)
Article Search
Decidable Subtyping of Existential Types for Julia
Julia Belyakova ORCID logo, Benjamin Chung ORCID logo, Ross Tate ORCID logo, and Jan Vitek ORCID logo
(Purdue University, USA; JuliaHub, USA; Independent Consultant, USA; Northeastern University, USA; Charles University, Czechia)
Preprint Archive submitted (1.7 MB) Info
RefinedRust: A Type System for High-Assurance Verification of Rust Programs
Lennard Gäher ORCID logo, Michael Sammler ORCID logo, Ralf Jung ORCID logo, Robbert KrebbersORCID logo, and Derek DreyerORCID logo
(MPI-SWS, Germany; ETH Zurich, Switzerland; Radboud University Nijmegen, Netherlands)
Article Search Info Artifacts Available Artifacts Reusable
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs
Longfei Qiu ORCID logo, Yoonseung Kim ORCID logo, Ji-Yong Shin ORCID logo, Jieung Kim ORCID logo, Wolf Honoré ORCID logo, and Zhong Shao ORCID logo
(Yale University, USA; Northeastern University, USA; Inha University, South Korea)
Article Search Artifacts Available Artifacts Reusable
Reducing Static Analysis Unsoundness with Approximate Interpretation
Mathias Rud Laursen ORCID logo, Wenyuan Xu ORCID logo, and Anders MøllerORCID logo
(Aarhus University, Denmark)
Preprint Artifacts Available Artifacts Reusable
Verification under Intel-x86 with Persistency
Parosh Abdulla ORCID logo, Mohamed Faouzi Atig ORCID logo, Ahmed Bouajjani ORCID logo, K. Narayan Kumar ORCID logo, and Prakash Saivasan ORCID logo
(Uppsala University, Sweden; Université Paris Cité, France; Chennai Mathematical Institute, India; Institute of Mathematical Sciences, India)
Article Search
Compilation of Modular and General Sparse Workspaces
Genghan Zhang ORCID logo, Olivia Hsu ORCID logo, and Fredrik Kjolstad ORCID logo
(Stanford University, USA)
Article Search
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation
Mridul AanjaneyaORCID logo and Santosh Nagarakatte ORCID logo
(Rutgers University, USA)
Article Search
Qubit Recycling Revisited
Hanru Jiang ORCID logo
(Beijing Institute of Mathematical Sciences and Applications, China)
Article Search Artifacts Reusable
A Lightweight Polyglot Code Transformation Language
Ameya Ketkar ORCID logo, Daniel RamosORCID logo, Lazaro Clapp ORCID logo, Raj Barik ORCID logo, and Murali Krishna Ramanathan ORCID logo
(Gitar, USA; Carnegie Mellon University, USA; INESC-ID, Portugal; Universidade de Lisboa, Portugal; Amazon Web Services, USA)
Article Search Artifacts Functional
An Algebraic Language for Specifying Quantum Networks
Anita Buckley ORCID logo, Pavel Chuprikov ORCID logo, Rodrigo Otoni ORCID logo, Robert Soulé ORCID logo, Robert RandORCID logo, and Patrick EugsterORCID logo
(USI Lugano, Switzerland; Yale University, USA; University of Chicago, USA)
Article Search Artifacts Available Artifacts Reusable
Linear Matching of JavaScript Regular Expressions
Aurèle Barrière ORCID logo and Clément Pit-Claudel ORCID logo
(EPFL, Switzerland)
Preprint Archive submitted (350 kB) Artifacts Available Artifacts Reusable
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving
Peixin Wang ORCID logo, Tengshun Yang ORCID logo, Hongfei Fu ORCID logo, Guanyan Li ORCID logo, and C.-H. Luke Ong ORCID logo
(Nanyang Technological University, Singapore; Institute of Software at Chinese Academy of Sciences, Beijing, China; University of Chinese Academy of Sciences, China; Shanghai Jiao Tong University, China; University of Oxford, United Kingdom)
Article Search Artifacts Available Artifacts Reusable
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata
Zhe Zhou ORCID logo, Qianchuan Ye ORCID logo, Benjamin DelawareORCID logo, and Suresh Jagannathan ORCID logo
(Purdue University, USA)
Preprint Artifacts Available Artifacts Reusable
Stream Types
Joseph W. Cutler ORCID logo, Christopher WatsonORCID logo, Emeka Nkurumeh ORCID logo, Phillip Hilliard ORCID logo, Harrison GoldsteinORCID logo, Caleb Stanford ORCID logo, and Benjamin C. Pierce ORCID logo
(University of Pennsylvania, USA; California Institute of Technology, USA; University of California at Davis, Davis, USA)
Article Search
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques
Elvira Albert ORCID logo, Maria Garcia de la Banda ORCID logo, Alejandro Hernández-Cerezo ORCID logo, Alexey Ignatiev ORCID logo, Albert Rubio ORCID logo, and Peter J. Stuckey ORCID logo
(Complutense University of Madrid, Spain; Monash University, Australia)
Article Search Artifacts Available Artifacts Reusable
Compiling Conditional Quantum Gates without Using Helper Qubits
Keli Huang ORCID logo and Jens PalsbergORCID logo
(University of California at Los Angeles, Los Angeles, USA)
Article Search Archive submitted (1.5 MB)
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties
Thibault DardinierORCID logo and Peter Müller ORCID logo
(ETH Zurich, Switzerland)
Article Search Artifacts Available Artifacts Reusable
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language
Gaurav Parthasarathy ORCID logo, Thibault DardinierORCID logo, Benjamin Bonneau ORCID logo, Peter Müller ORCID logo, and Alexander J. Summers ORCID logo
(ETH Zurich, Switzerland; Université Grenoble Alpes - CNRS - Grenoble INP - VERIMAG, France; University of British Columbia, Canada)
Article Search Artifacts Available Artifacts Reusable
Live Verification in an Interactive Proof Assistant
Samuel Gruetter ORCID logo, Viktor Fukala ORCID logo, and Adam ChlipalaORCID logo
(Massachusetts Institute of Technology, USA)
Article Search Archive submitted (440 kB) Artifacts Available Artifacts Reusable
Bringing the WebAssembly Standard up to Speed with SpecTec
Dongjun YounORCID logo, Wonho Shin ORCID logo, Jaehyun Lee ORCID logo, Sukyoung RyuORCID logo, Joachim BreitnerORCID logo, Philippa Gardner ORCID logo, Sam Lindley ORCID logo, Matija Pretnar ORCID logo, Xiaojia Rao ORCID logo, Conrad Watt ORCID logo, and Andreas RossbergORCID logo
(KAIST, South Korea; Independent, Germany; Imperial College London, United Kingdom; University of Edinburgh, United Kingdom; University of Ljubljana, Slovenia; University of Cambridge, United Kingdom)
Article Search Artifacts Available Artifacts Functional
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric
Atsushi IgarashiORCID logo, Shota Ozaki ORCID logo, Taro Sekiyama ORCID logo, and Yudai TanabeORCID logo
(Kyoto University, Japan; National Institute of Informatics, Japan; SOKENDAI, Japan; Tokyo Institute of Technology, Japan)
Article Search Archive submitted (930 kB)
Quest Complete: The Holy Grail of Gradual Security
Tianyu ChenORCID logo and Jeremy G. Siek ORCID logo
(Indiana University, USA)
Preprint Archive submitted (360 kB) Artifacts Available Artifacts Reusable
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding
Qiuping Yi ORCID logo, Yifan Yu ORCID logo, and Guowei Yang ORCID logo
(Beijing University of Posts and Telecommunications, China; University of Queensland, Australia)
Article Search Artifacts Available Artifacts Reusable
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly
Michael Fitzgibbons ORCID logo, Zoe Paraskevopoulou ORCID logo, Noble Mushtak ORCID logo, Michelle Thalakottur ORCID logo, Jose Sulaiman Manzur ORCID logo, and Amal AhmedORCID logo
(Northeastern University, USA; Ethereum Foundation, Germany)
Article Search Artifacts Reusable
SpEQ: Translation of Sparse Codes using Equivalences
Avery Laird ORCID logo, Bangtian Liu ORCID logo, Nikolaj Bjørner ORCID logo, and Maryam Mehri DehnaviORCID logo
(University of Toronto, Canada; Microsoft Research, USA)
Article Search Artifacts Available Artifacts Reusable
Foundational Integration Verification of a Cryptographic Server
Andres ErbsenORCID logo, Jade Philipoom ORCID logo, Dustin Jamner ORCID logo, Ashley Lin ORCID logo, Samuel Gruetter ORCID logo, Clément Pit-Claudel ORCID logo, and Adam ChlipalaORCID logo
(Google, USA; Google, Germany; Massachusetts Institute of Technology, USA; EPFL, Switzerland)
Article Search Artifacts Available Artifacts Reusable
Reward-Guided Synthesis of Intelligent Agents with Control Structures
Guofeng Cui ORCID logo, Yuning Wang ORCID logo, Wenjie Qiu ORCID logo, and He ZhuORCID logo
(Rutgers University, USA)
Article Search Info Artifacts Reusable
Compiling Probabilistic Programs for Variable Elimination with Information Flow
Jianlin LiORCID logo, Eric Wang ORCID logo, and Yizhou ZhangORCID logo
(University of Waterloo, Canada)
Article Search Artifacts Reusable
SPORE: Combining Symmetry and Partial Order Reduction
Michalis KokologiannakisORCID logo, Iason Marmanis ORCID logo, and Viktor VafeiadisORCID logo
(MPI-SWS, Germany)
Article Search Info Artifacts Reusable
Predictable Verification using Intrinsic Definitions
Adithya MuraliORCID logo, Cody RiveraORCID logo, and P. MadhusudanORCID logo
(University of Illinois at Urbana-Champaign, USA)
Article Search Archive submitted (760 kB) Artifacts Available Artifacts Reusable
Context-Free Language Reachability via Skewed Tabulation
Yuxiang Lei ORCID logo, Camille Bossut ORCID logo, Yulei Sui ORCID logo, and Qirun Zhang ORCID logo
(UNSW, Australia; Georgia Institute of Technology, USA)
Article Search Archive submitted (810 kB) Artifacts Available Artifacts Reusable
Falcon: A Scalable Analytical Cache Model
Arjun Pitchanathan ORCID logo, Kunwar Grover ORCID logo, and Tobias Grosser ORCID logo
(University of Edinburgh, United Kingdom; Advanced Micro Devices, United Kingdom; University of Cambridge, United Kingdom)
Article Search Artifacts Available Artifacts Reusable
Equivalence by Canonicalization for Synthesis-Backed Refactoring
Justin LubinORCID logo, Jeremy Ferguson ORCID logo, Kevin Ye ORCID logo, Jacob Yim ORCID logo, and Sarah E. ChasinsORCID logo
(University of California at Berkeley, Berkeley, USA)
Article Search Archive submitted (750 kB) Artifacts Available Artifacts Reusable
KATch: A Fast Symbolic Verifier for NetKAT
Mark Moeller ORCID logo, Jules JacobsORCID logo, Olivier Savary Belanger ORCID logo, David Darais ORCID logo, Cole Schlesinger ORCID logo, Steffen Smolka ORCID logo, Nate FosterORCID logo, and Alexandra Silva ORCID logo
(Cornell University, USA; Galois, USA; Google, USA)
Article Search Artifacts Reusable
Hyperblock Scheduling for Verified High-Level Synthesis
Yann HerklotzORCID logo and John Wickerson ORCID logo
(Imperial College London, United Kingdom)
Preprint Artifacts Available Artifacts Reusable
Numerical Fuzz: A Type System for Rounding Error Analysis
Ariel E. Kellison ORCID logo and Justin Hsu ORCID logo
(Cornell University, USA)
Article Search Artifacts Available Artifacts Reusable
Inductive Approach to Spacer
Takeshi Tsukada ORCID logo and Hiroshi UnnoORCID logo
(Chiba University, Japan; Tohoku University, Japan)
Article Search Info
V-Star: Learning Visibly Pushdown Grammars from Program Inputs
Xiaodong Jia ORCID logo and Gang TanORCID logo
(Pennsylvania State University, USA)
Article Search Archive submitted (800 kB) Artifacts Reusable
Hashing Modulo Context-Sensitive 𝛼-Equivalence
Lasse Blaauwbroek ORCID logo, Miroslav Olšák ORCID logo, and Herman Geuvers ORCID logo
(Institut des Hautes Études Scientifiques, France; Radboud University Nijmegen, Netherlands)
Preprint Artifacts Available Artifacts Reusable
Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments
Gabriel Matute ORCID logo, Wode Ni ORCID logo, Titus Barik ORCID logo, Alvin Cheung ORCID logo, and Sarah E. ChasinsORCID logo
(University of California at Berkeley, Berkeley, USA; Carnegie Mellon University, USA; Apple, USA)
Article Search Artifacts Functional
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions
Konstantinos Mamouras ORCID logo, Alexis Le Glaunec ORCID logo, Wu Angela Li ORCID logo, and Agnishom Chattopadhyay ORCID logo
(Rice University, USA)
Article Search
Equivalence and Similarity Refutation for Probabilistic Programs
Krishnendu Chatterjee ORCID logo, Ehsan Kafshdar Goharshady ORCID logo, Petr Novotný ORCID logo, and Đorđe Žikelić ORCID logo
(IST Austria, Austria; Masaryk University, Czechia; Singapore Management University, Singapore)
Preprint Artifacts Available Artifacts Reusable
Probabilistic Programming with Programmable Variational Inference
McCoy R. Becker ORCID logo, Alexander K. LewORCID logo, Xiaoyan Wang ORCID logo, Matin Ghavami ORCID logo, Mathieu Huot ORCID logo, Martin C. Rinard ORCID logo, and Vikash K. MansinghkaORCID logo
(Massachusetts Institute of Technology, USA)
Article Search Info Artifacts Available Artifacts Reusable
PL4XGL: A Programming Language Approach to Explainable Graph Learning
Minseok Jeon ORCID logo, Jihyeok ParkORCID logo, and Hakjoo Oh ORCID logo
(Korea University, South Korea)
Article Search Archive submitted (680 kB) Artifacts Available
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation
Ruslan NikolaevORCID logo and Binoy Ravindran ORCID logo
(Pennsylvania State University, USA; Virginia Tech, USA)
Preprint Info Artifacts Available Artifacts Reusable

proc time: 14.66