default search action
Google
Google Scholar
Semantic Scholar
Internet Archive Scholar
CiteSeerX
ORCIDProceedings of the ACM on Programming Languages, Volume 8
Volume 8, Number POPL, January 2024
POPL 2024
- Pascal Bergsträßer
, Moses Ganardi, Anthony W. Lin, Georg Zetzsche:
Ramsey Quantifiers in Linear Arithmetics. 1-32 - Jens Oliver Gutsfeld, Markus Müller-Olm, Christoph Ohrem:
Deciding Asynchronous Hyperproperties for Recursive Programs. 33-60 - Xueying Qin, Liam O'Connor, Rob van Glabbeek, Peter Höfner, Ohad Kammar, Michel Steuwer:
Shoggoth: A Formal Foundation for Strategic Rewriting. 61-89 - A. R. Balasubramanian, Rupak Majumdar, Ramanathan S. Thinniyam, Georg Zetzsche:
Reachability in Continuous Pushdown VASS. 90-114 - Fuga Kawamata, Hiroshi Unno, Taro Sekiyama, Tachio Terauchi:
Answer Refinement Modification: Refinement Type System for Algebraic Effects and Handlers. 115-147 - William Mansky, Ke Du:
An Iris Instance for Verifying CompCert C Programs. 148-174 - Patrick Cousot:
Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation. 175-208 - Antoine Van Muylder, Andreas Nuyts, Dominique Devriese:
Internal and Observational Parametricity for Cubical Agda. 209-240 - Amin Timany, Simon Oddershede Gregersen, Léo Stefanesco, Jonas Kastberg Hinrichsen, Léon Gondelman, Abel Nieto, Lars Birkedal:
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement. 241-272 - Harrison Grodin, Yue Niu, Jonathan Sterling, Robert Harper:
Decalf: A Directed, Effectful Cost-Aware Logical Framework. 273-301 - Alexandre Moine, Sam Westrick, Stephanie Balzer:
DisLog: A Separation Logic for Disentanglement. 302-331 - Dan Frumin, Amin Timany, Lars Birkedal:
Modular Denotational Semantics for Effects with Guarded Interaction Trees. 332-361 - Takeshi Tsukada, Kazuyuki Asada:
Enriched Presheaf Model of Quantum FPC. 362-392 - Guannan Wei, Oliver Bracevac, Songlin Jia, Yuyan Bao, Tiark Rompf:
Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic Programs. 393-424 - Andrei Popescu:
Nominal Recursors as Epi-Recursors. 425-456 - Stephen Mell, Steve Zdancewic, Osbert Bastani:
Optimal Program Synthesis via Abstract Interpretation. 457-481 - Francis Rinaldi, june wunder, Arthur Azevedo de Amorim, Stefan K. Muller:
Pipelines and Beyond: Graph Types for ADTs with Futures. 482-511 - Noah Patton, Kia Rahmani, Meghana Missula, Joydeep Biswas, Isil Dillig:
Programming-by-Demonstration for Long-Horizon Robot Tasks. 512-545 - Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry:
With a Few Square Roots, Quantum Computing Is as Easy as Pi. 546-574 - Amin Timany, Armaël Guéneau, Lars Birkedal:
The Logical Essence of Well-Bracketed Control Flow. 575-603 - Angus Hammond, Zongyuan Liu, Thibaut Pérami, Peter Sewell, Lars Birkedal, Jean Pichon-Pharabod:
An Axiomatic Basis for Computer Programming on the Relaxed Arm-A Architecture: The AxSL Logic. 604-637 - Chih-Duo Hong, Anthony W. Lin:
Regular Abstractions for Array Systems. 638-666 - Will Crichton, Shriram Krishnamurthi:
A Core Calculus for Documents: Or, Lambda: The Ultimate Document. 667-694 - Filip Sieczkowski, Sergei Stepanenko, Jonathan Sterling, Lars Birkedal:
The Essence of Generalized Algebraic Data Types. 695-723 - John Cyphert, Zachary Kincaid:
Solvable Polynomial Ideals: The Ideal Reflection for Program Analysis. 724-752 - Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Asynchronous Probabilistic Couplings in Higher-Order Separation Logic. 753-784 - Brandon Hewer, Graham Hutton:
Quotient Haskell: Lightweight Quotient Types for All. 785-815 - Shankara Pailoor, Yuepeng Wang, Isil Dillig:
Semantic Code Refactoring for Abstract Data Types. 816-847 - Pu Sun, Fu Song, Yuqi Chen, Taolue Chen:
EasyBC: A Cryptography-Specific Language for Security Analysis of Block Ciphers against Differential Cryptanalysis. 848-881 - Julian Müllner, Marcel Moosbrugger, Laura Kovács:
Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs. 882-910 - Azadeh Farzan, Umang Mathur:
Coarser Equivalences for Causal Concurrency. 911-941 - Ian Briggs, Yash Lad, Pavel Panchekha:
Implementation and Synthesis of Math Library Functions. 942-969 - Neta Elad, Oded Padon, Sharon Shoham:
An Infinite Needle in a Finite Haystack: Finding Infinite Counter-Models in Deductive Verification. 970-1000 - Alex Buna-Marginean, Vincent Cheval, Mahsa Shirmohammadi, James Worrell:
On Learning Polynomial Recursive Programs. 1001-1027 - Jianan Yao, Runzhou Tao, Ronghui Gu, Jason Nieh:
Mostly Automated Verification of Liveness Properties for Distributed Protocols with Ranking Functions. 1028-1059 - Tom Smeding, Matthijs Vákár:
Efficient CHAD. 1060-1088 - Rupak Majumdar, V. R. Sathiyanarayana:
Positive Almost-Sure Termination: Complexity and Proof Rules. 1089-1117 - Sam Westrick, Matthew Fluet, Mike Rainey, Umut A. Acar:
Automatic Parallelism Management. 1118-1149 - Simon Guilloud, Viktor Kuncak:
Orthologic with Axioms. 1150-1178 - Giuseppe Castagna, Mickaël Laurent, Kim Nguyen:
Polymorphic Type Inference for Dynamic Languages. 1179-1210 - Xing Zhang, Ruifeng Xie, Guanchen Guo, Xiao He, Tao Zan, Zhenjiang Hu:
Fusing Direct Manipulations into Functional Programs. 1211-1238 - Shankaranarayanan Krishna, Aniket Lal, Andreas Pavlogiannis, Omkar Tuppe:
On-the-Fly Static Analysis via Dynamic Bidirected Dyck Reachability. 1239-1268 - Lorenzo Ceragioli, Fabio Gadducci, Giuseppe Lomurno, Gabriele Tedeschi:
Quantum Bisimilarity via Barbs and Contexts: Curbing the Power of Non-deterministic Observers. 1269-1297 - Yiyun Liu, Jonathan Chan, Jessica Shi, Stephanie Weirich:
Internalizing Indistinguishability with Dependent Types. 1298-1325 - Mikolaj Bojanczyk, Bartek Klin:
Polyregular Functions on Unordered Trees of Bounded Height. 1326-1351 - Liron Cohen, Adham Jabarin, Andrei Popescu, Reuben N. S. Rowe:
The Complex(ity) Landscape of Checking Infinite Descent. 1352-1384 - Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers:
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. 1385-1417 - Lionel Parreaux, Aleksander Boruch-Gruszecki, Andong Fan, Chun Yin Chau:
When Subtyping Constraints Liberate: A Novel Type Inference Approach for First-Class Polymorphism. 1418-1450 - Lyes Attouche, Mohamed-Amine Baazizi, Dario Colazzo, Giorgio Ghelli, Carlo Sartiani, Stefanie Scherzinger:
Validation of Modern JSON Schema: Formalization and Complexity. 1451-1481 - François Pottier, Armaël Guéneau, Jacques-Henri Jourdan, Glen Mével:
Thunks and Debits in Separation Logic with Time Credits. 1482-1508 - Nicolas Chataing, Stephen Dolan, Gabriel Scherer, Jeremy Yallop:
Unboxed Data Constructors: Or, How cpp Decides a Halting Problem. 1509-1539 - Xiang Li, Xiangyu Zhou, Rui Dong, Yihong Zhang, Xinyu Wang:
Efficient Bottom-Up Synthesis for Programs with Local Variables. 1540-1568 - Jatin Arora, Stefan K. Muller, Umut A. Acar:
Disentanglement with Futures, State, and Interaction. 1569-1599 - Wenhao Tang, Daniel Hillerström, Sam Lindley, J. Garrett Morris:
Soundly Handling Linearity. 1600-1628 - Marco Campion, Mila Dalla Preda, Roberto Giacobazzi, Caterina Urban:
Monotonicity and the Precision of Program Analysis. 1629-1662 - Donnacha Oisín Kidney, Zhixuan Yang, Nicolas Wu:
Algebraic Effects Meet Hoare Logic in Cubical Agda. 1663-1695 - Philippe Heim, Rayna Dimitrova:
Solving Infinite-State Games via Acceleration. 1696-1726 - Thomas Koehler, Andrés Goens, Siddharth Bhat, Tobias Grosser, Phil Trinder, Michel Steuwer:
Guided Equality Saturation. 1727-1758 - Haowei Deng, Runzhou Tao, Yuxiang Peng, Xiaodi Wu:
A Case for Synthesis of Recursive Quantum Unitary Programs. 1759-1788 - Joshua M. Cohen, Philip Johnson-Freyd:
A Formalization of Core Why3 in Coq. 1789-1818 - Nathanael L. Ackerman, Cameron E. Freer, Younesse Kaddar, Jacek Karwowski, Sean K. Moss, Daniel M. Roy, Sam Staton, Hongseok Yang:
Probabilistic Programming Interfaces for Random Graphs: Markov Categories, Graphons, and Nominal Sets. 1819-1849 - Thodoris Sotiropoulos, Stefanos Chaliasos, Zhendong Su:
API-Driven Program Synthesis for Testing Static Typing Implementations. 1850-1881 - Francesca Randone, Luca Bortolussi, Emilio Incerto, Mirco Tribastone:
Inference of Probabilistic Programs with Moment-Matching Gaussian Mixtures. 1882-1912 - Itsaka Rakotonirina, Gilles Barthe, Clara Schneidewind:
Decision and Complexity of Dolev-Yao Hyperproperties. 1913-1944 - Matthew Hague, Artur Jez, Anthony W. Lin:
Parikh's Theorem Made Symbolic. 1945-1977 - Soham Chakraborty, Shankara Narayanan Krishna, Umang Mathur, Andreas Pavlogiannis:
How Hard Is Weak-Memory Testing? 1978-2009 - Steven Ramsay, Charlie Walpole:
Ill-Typed Programs Don't Evaluate. 2010-2040 - Eric Zhao, Raef Maroof, Anand Dukkipati, Andrew Blinn, Zhiyi Pan, Cyrus Omar:
Total Type Error Localization and Recovery with Holes. 2041-2068 - Litao Zhou, Jianxing Qin, Qinshi Wang, Andrew W. Appel, Qinxiang Cao:
VST-A: A Foundationally Sound Annotation Verifier. 2069-2098 - Michael Borkowski, Niki Vazou, Ranjit Jhala:
Mechanizing Refinement Types. 2099-2128 - Yuantian Ding, Xiaokang Qiu:
Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipulations. 2129-2159 - Ling Zhang, Yuting Wang, Jinhua Wu, Jérémie Koenig, Zhong Shao:
Fully Composable and Adequate Verified Compilation with Direct Refinements between Open Modules. 2160-2190 - Zhendong Ang, Umang Mathur:
Predictive Monitoring against Pattern Regular Languages. 2191-2225 - Cezar-Constantin Andrici, Stefan Ciobaca, Catalin Hritcu, Guido Martínez, Exequiel Rivas, Éric Tanter, Théo Winterhalter:
Securing Verified IO Programs Against Unverified Code in F. 2226-2259 - Zhongkui Ma, Jiaying Li, Guangdong Bai:
ReLU Hull Approximation. 2260-2287 - Robert Atkey:
Polynomial Time and Dependent Types. 2288-2317 - Justin Frank, Benjamin Quiring, Leonidas Lampropoulos:
Generating Well-Typed Terms That Are Not "Useless". 2318-2339 - Thorsten Altenkirch, Yorgo Chamoun, Ambrus Kaposi, Michael Shulman:
Internal Parametricity, without an Interval. 2340-2369 - Martin Elsman:
Explicit Effects and Effect Constraints in ReML. 2370-2394 - Adam T. Geller, Justin Frank, William J. Bowman:
Indexed Types for a Statically Safe WebAssembly. 2395-2424 - Yuxiang Peng, Jacob Young, Pengyu Liu, Xiaodi Wu:
SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog Compilation. 2425-2455 - Prasad Jayanti, Siddhartha Jayanti, Ugur Y. Yavuz, Lizzie Hernandez:
A Universal, Sound, and Complete Forward Reasoning Technique for Machine-Verified Proofs of Linearizability. 2456-2484 - Azadeh Farzan, Dominik Klumpp, Andreas Podelski:
Commutativity Simplifies Proofs of Parameterized Programs. 2485-2513 - Claudia Faggian, Daniele Pautasso, Gabriele Vanoni:
Higher Order Bayesian Networks, Exactly. 2514-2546 - Conrad Zimmerman, Jenna DiVincenzo, Jonathan Aldrich:
Sound Gradual Verification with Symbolic Execution. 2547-2576 - Supun Abeysinghe, Anxhelo Xhebraj, Tiark Rompf:
Flan: An Expressive and Efficient Datalog Compiler for Program Analysis. 2577-2609 - Ugo Dal Lago, Alexis Ghyselen:
On Model-Checking Higher-Order Effectful Programs. 2610-2638 - Cameron Moy, Christos Dimoulas, Matthias Felleisen:
Effectful Software Contracts. 2639-2666 - John Peter Campora III, Mohammad Wahiduzzaman Khan, Sheng Chen:
Type-Based Gradual Typing Performance Optimization. 2667-2699 - Henry DeYoung, Andreia Mordido, Frank Pfenning, Ankush Das:
Parametric Subtyping for Structural Parametric Polymorphism. 2700-2730 - Yanis Sellami, Guillaume Girol, Frédéric Recoules, Damien Couroussé, Sébastien Bardin:
Inference of Robust Reachability Constraints. 2731-2760 - Konstantinos Mamouras, Agnishom Chattopadhyay:
Efficient Matching of Regular Expressions with Lookaround Assertions. 2761-2791 - Kevin Batz, Tom Jannik Biskup, Joost-Pieter Katoen, Tobias Winkler:
Programmatic Strategy Synthesis: Resolving Nondeterminism in Probabilistic Programs. 2792-2820
Volume 8, Number PLDI, 2024
PLDI 2024
- Debangshu Banerjee, Changming Xu, Gagandeep Singh:
Input-Relational Verification of Deep Neural Networks. 1-27 - Minseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao, Jeehoon Kang:
Modular Hardware Design of Pipelined Circuits with Hazards. 28-51 - Yannick Forster, Matthieu Sozeau, Nicolas Tabareau:
Verified Extraction from Coq to OCaml. 52-75 - Long Pham, Feras A. Saad, Jan Hoffmann:
Robust Resource Bounds with Static Analysis and Bayesian Inference. 76-101 - Qiantan Hong, Alex Aiken:
Recursive Program Synthesis using Paramorphisms. 102-125 - Aleksandar Krastev, Nikola Samardzic, Simon Langowski, Srinivas Devadas, Daniel Sánchez:
A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic Encryption. 126-150 - Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang:
Concurrent Immediate Reference Counting. 151-174 - Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang:
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. 175-198 - Siva Kesava Reddy Kakarla, Francis Y. Yan, Ryan Beckett:
Diffy: Data-Driven Bug Finding for Configurations. 199-222 - Shaohua Li, Theodoros Theodoridis, Zhendong Su:
Boosting Compiler Testing by Injecting Real-World Code. 223-245 - Benjamin Mikek, Qirun Zhang:
SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories. 246-271 - Ritvik Sharma, Sara Achour:
Compilation of Qubit Circuits to Optimized Qutrit Circuits. 272-295 - Aditya Anand, Solai Adithya, Swapnil Rustagi, Priyam Seth, Vijay Sundaresan, Daryl Maier, V. Krishna Nandivada, Manas Thakur:
Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes. 296-319 - Amanda Liu, Gilbert Bernstein, Adam Chlipala, Jonathan Ragan-Kelley:
A Verified Compiler for a Functional Tensor Language. 320-342 - Chujun Geng, Spyros Blanas, Michael D. Bond, Yang Wang:
IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly Isolated Data Store Applications. 343-367 - Dorian Lesbre, Matthieu Lemerre:
Compiling with Abstract Interpretation. 368-393 - Matthew Lutze, Magnus Madsen:
Associated Effects: Flexible Abstractions for Effectful Programming. 394-416 - Mafalda Ferreira, Miguel Monteiro, Tiago Brito, Miguel E. Coimbra, Nuno Santos, Limin Jia, José Fragoso Santos:
Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs. 417-441 - Joao Rivera, Franz Franchetti, Markus Püschel:
Floating-Point TVPI Abstract Domain. 442-466 - Ajay Brahmakshatriya, Christopher Rinard, Manya Ghobadi, Saman P. Amarasinghe:
NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks. 467-491 - Charles Yuan, Michael Carbin:
The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation. 492-517 - Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley:
The Functional Essence of Imperative Binary Search Trees. 518-542 - Mikhail Svyatlovskiy, Shai Mermelstein, Ori Lahav:
Compositional Semantics for Shared-Variable Concurrency. 543-566 - Peisen Yao, Jinguo Zhou, Xiao Xiao, Qingkai Shi, Rongxin Wu, Charles Zhang:
Falcon: A Fused Approach to Path-Sensitive Sparse Data Dependence Analysis. 567-592 - Hongzheng Chen, Niansong Zhang, Shaojie Xiang, Zhichen Zeng, Mengjia Dai, Zhiru Zhang:
Allo: A Programming Model for Composable Accelerator Design. 593-620 - Joseph Raskind, Timur Babakol, Khaled Mahmoud, Yu David Liu:
VESTA: Power Modeling with Language Runtime Events. 621-646 - Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman P. Amarasinghe, Ilya Sergey:
Mechanised Hypersafety Proofs about Structured Data. 647-670 - Theodoros Theodoridis, Zhendong Su:
Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior. 671-691 - Thomas Ball, Peli de Halleux, James Devine, Steve Hodges, Michal Moskal:
Jacdac: Service-Based Prototyping of Embedded Systems. 692-715 - Jaemin Hong, Sukyoung Ryu:
Don't Write, but Return: Replacing Output Parameters with Algebraic Data Types in C-to-Rust Translation. 716-740 - Guillaume Girol, Guilhem Lacombe, Sébastien Bardin:
Quantitative Robustness for Vulnerability Assessment. 741-765 - George Zakhour, Pascal Weisenburger, Guido Salvaneschi:
Automated Verification of Fundamental Algebraic Laws. 766-789 - Mathieu Huot, Matin Ghavami, Alexander K. Lew, Ulrich Schaechtle, Cameron E. Freer, Zane Shelby, Martin C. Rinard, Feras A. Saad, Vikash K. Mansinghka:
GenSQL: A Probabilistic Programming System for Querying Generative Models of Database Tables. 790-815 - Iavor S. Diatchki, Mike Dodds, Harrison Goldstein, Bill Harris, David A. Holland, Benoît Razet, Cole Schlesinger, Simon Winwood:
Daedalus: Safer Document Parsing. 816-840 - Bastian Köpcke, Sergei Gorlatch, Michel Steuwer:
Descend: A Safe GPU Systems Programming Language. 841-864 - Poorva Garg, Steven Holtzen, Guy Van den Broeck, Todd D. Millstein:
Bit Blasting Probabilistic Programs. 865-888 - Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer:
Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq. 889-913 - Jiawen Liu, Weihao Qu, Marco Gaboardi, Deepak Garg, Jonathan R. Ullman:
Program Analysis for Adaptive Data Analysis. 914-938 - Ruyi Ji, Yuwei Zhao, Nadia Polikarpova, Yingfei Xiong, Zhenjiang Hu:
Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis. 939-964 - Guannan Wei, Danning Xie, Wuqi Zhang, Yongwei Yuan, Zhuo Zhang:
Consolidating Smart Contracts with Behavioral Contracts. 965-989 - Christian Wimmer, Codrut Stancu, David Kozak, Thomas Würthinger:
Scaling Type-Based Points-to Analysis with Saturation. 990-1013 - Ziteng Wang, Shankara Pailoor, Aaryan Prakash, Yuepeng Wang, Isil Dillig:
From Batch to Stream: Automatic Generation of Online Algorithms. 1014-1039 - Wang Fang, Mingsheng Ying:
Symbolic Execution for Quantum Error Correction Programs. 1040-1065 - Blake Pelton, Adam Sapek, Ken Eguro, Daniel Lo, Alessandro Forin, Matt Humphrey, Jinwen Xi, David Cox, Rajas Karandikar, Johannes de Fine Licht, Evgeny Babin, Adrian M. Caulfield, Doug Burger:
Wavefront Threading Enables Effective High-Level Synthesis. 1066-1090 - Julia Belyakova, Benjamin Chung, Ross Tate, Jan Vitek:
Decidable Subtyping of Existential Types for Julia. 1091-1114 - Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer:
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. 1115-1139 - Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honoré, Zhong Shao:
LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs. 1140-1164 - Mathias Rud Laursen, Wenyuan Xu, Anders Møller:
Reducing Static Analysis Unsoundness with Approximate Interpretation. 1165-1188 - Parosh Aziz Abdulla, Mohamed Faouzi Atig, Ahmed Bouajjani, K. Narayan Kumar, Prakash Saivasan:
Verification under Intel-x86 with Persistency. 1189-1212 - Genghan Zhang, Olivia Hsu, Fredrik Kjolstad:
Compilation of Modular and General Sparse Workspaces. 1213-1238 - Mridul Aanjaneya, Santosh Nagarakatte:
Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear Programs with Convex Hull as the Intermediate Representation. 1239-1263 - Hanru Jiang:
Qubit Recycling Revisited. 1264-1287 - Ameya Ketkar, Daniel Ramos, Lazaro Clapp, Raj Barik, Murali Krishna Ramanathan:
A Lightweight Polyglot Code Transformation Language. 1288-1312 - Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, Patrick Eugster:
An Algebraic Language for Specifying Quantum Networks. 1313-1335 - Aurèle Barrière, Clément Pit-Claudel:
Linear Matching of JavaScript Regular Expressions. 1336-1360 - Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, C.-H. Luke Ong:
Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving. 1361-1386 - Zhe Zhou, Qianchuan Ye, Benjamin Delaware, Suresh Jagannathan:
A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite Automata. 1387-1411 - Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, Benjamin C. Pierce:
Stream Types. 1412-1436 - Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, Peter J. Stuckey:
SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT Techniques. 1437-1462 - Keli Huang, Jens Palsberg:
Compiling Conditional Quantum Gates without Using Helper Qubits. 1463-1484 - Thibault Dardinier, Peter Müller:
Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties. 1485-1509 - Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers:
Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into an Intermediate Verification Language. 1510-1534 - Samuel Gruetter, Viktor Fukala, Adam Chlipala:
Live Verification in an Interactive Proof Assistant. 1535-1558 - Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas Rossberg:
Bringing the WebAssembly Standard up to Speed with SpecTec. 1559-1584 - Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, Yudai Tanabe:
Space-Efficient Polymorphic Gradual Typing, Mostly Parametric. 1585-1608 - Tianyu Chen, Jeremy G. Siek:
Quest Complete: The Holy Grail of Gradual Security. 1609-1632 - Qiuping Yi, Yifan Yu, Guowei Yang:
Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding. 1633-1655 - Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur, Amal Ahmed:
RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly. 1656-1679 - Avery Laird, Bangtian Liu, Nikolaj S. Bjørner, Maryam Mehri Dehnavi:
SpEQ: Translation of Sparse Codes using Equivalences. 1680-1703 - Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala:
Foundational Integration Verification of a Cryptographic Server. 1704-1729 - Guofeng Cui, Yuning Wang, Wenjie Qiu, He Zhu:
Reward-Guided Synthesis of Intelligent Agents with Control Structures. 1730-1754 - Jianlin Li, Eric Wang, Yizhou Zhang:
Compiling Probabilistic Programs for Variable Elimination with Information Flow. 1755-1780 - Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis:
SPORE: Combining Symmetry and Partial Order Reduction. 1781-1803 - Adithya Murali, Cody Rivera, P. Madhusudan:
Predictable Verification using Intrinsic Definitions. 1804-1829 - Yuxiang Lei, Camille Bossut, Yulei Sui, Qirun Zhang:
Context-Free Language Reachability via Skewed Tabulation. 1830-1853 - Arjun Pitchanathan, Kunwar Grover, Tobias Grosser:
Falcon: A Scalable Analytical Cache Model. 1854-1878 - Justin Lubin, Jeremy Ferguson, Kevin Ye, Jacob Yim, Sarah E. Chasins:
Equivalence by Canonicalization for Synthesis-Backed Refactoring. 1879-1904 - Mark Moeller, Jules Jacobs, Olivier Savary Bélanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, Alexandra Silva:
KATch: A Fast Symbolic Verifier for NetKAT. 1905-1928 - Yann Herklotz, John Wickerson:
Hyperblock Scheduling for Verified High-Level Synthesis. 1929-1953 - Ariel E. Kellison, Justin Hsu:
Numerical Fuzz: A Type System for Rounding Error Analysis. 1954-1978 - Takeshi Tsukada, Hiroshi Unno:
Inductive Approach to Spacer. 1979-2002 - Xiaodong Jia, Gang Tan:
V-Star: Learning Visibly Pushdown Grammars from Program Inputs. 2003-2026 - Lasse Blaauwbroek, Miroslav Olsák, Herman Geuvers:
Hashing Modulo Context-Sensitive 𝛼-Equivalence. 2027-2050 - Gabriel Matute, Wode Ni, Titus Barik, Alvin Cheung, Sarah E. Chasins:
Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with Incomplete Code Fragments. 2051-2072 - Konstantinos Mamouras, Alexis Le Glaunec, Wu Angela Li, Agnishom Chattopadhyay:
Static Analysis for Checking the Disambiguation Robustness of Regular Expressions. 2073-2097 - Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Dorde Zikelic:
Equivalence and Similarity Refutation for Probabilistic Programs. 2098-2122 - McCoy R. Becker, Alexander K. Lew, Xiaoyan Wang, Matin Ghavami, Mathieu Huot, Martin C. Rinard, Vikash K. Mansinghka:
Probabilistic Programming with Programmable Variational Inference. 2123-2147 - Minseok Jeon, Jihyeok Park, Hakjoo Oh:
PL4XGL: A Programming Language Approach to Explainable Graph Learning. 2148-2173 - Ruslan Nikolaev, Binoy Ravindran:
A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation. 2174-2198
Volume 8, Number OOPSLA1, 2024
OOPSLA 2024 - Part 1
- Charles Yuan, Agnes Villanyi, Michael Carbin:
Quantum Control Machine: The Limits of Control Flow in Quantum Programming. 1-28 - Will Crichton, Shriram Krishnamurthi:
Profiling Programming Language Learning. 29-54 - Anouk Paradis, Jasper Dekoninck, Benjamin Bichsel, Martin T. Vechev:
Synthetiq: Fast and Versatile Quantum Circuit Synthesis. 55-82 - Aashish Yadavally, Yi Li, Shaohua Wang, Tien N. Nguyen:
A Learning-Based Approach to Static Program Slicing. 83-109 - Chi Zhang, Linzhang Wang, Manuel Rigger:
Finding Cross-Rule Optimization Bugs in Datalog Engines. 110-136 - Jie Liu, Zhongyuan Zhao, Zijian Ding, Benjamin Brock, Hongbo Rong, Zhiru Zhang:
UniSparse: An Intermediate Language for General Sparse Format Customization. 137-165 - Ada Lamba, Max Taylor, Vincent Beardsley, Jacob Bambeck, Michael D. Bond, Zhiqiang Lin:
Cocoon: Static Information Flow Control in Rust. 166-193 - Clement Blaudeau, Didier Rémy, Gabriel Radanne:
Fulfilling OCaml Modules with Transparency. 194-222 - Anoud Alshnakat, Didrik Lundberg, Roberto Guanciale, Mads Dam:
HOL4P4: Mechanized Small-Step Semantics for P4. 223-249 - Shiv Sundram, Muhammad Usman Tariq, Fredrik Kjolstad:
Compiling Recurrences over Dense and Sparse Arrays. 250-275 - Noam Zilberstein, Angelina Saliling, Alexandra Silva:
Outcome Separation Logic: Local Reasoning for Correctness and Incorrectness with Computational Effects. 276-304 - Di Wang, Thomas W. Reps:
Newtonian Program Analysis of Probabilistic Programs. 305-333 - Kuang-Chen Lu, Shriram Krishnamurthi:
Identifying and Correcting Programming Language Behavior Misconceptions. 334-361 - Krishnendu Chatterjee, Amir Kafshdar Goharshady, Tobias Meggendorfer, Dorde Zikelic:
Quantitative Bounds on Resource Usage of Probabilistic Programs. 362-391 - Yangruibo Ding, Marcus J. Min, Gail E. Kaiser, Baishakhi Ray:
CYCLE: Learning to Self-Refine the Code Generation. 392-418 - Wolf Honoré, Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Zhong Shao:
AdoB: Bridging Benign and Byzantine Consensus with Atomic Distributed Objects. 419-448 - Ziyang Xu, Yebin Chon, Yian Su, Zujun Tan, Sotiris Apostolakis, Simone Campanoni, David I. August:
PROMPT: A Fast and Extensible Memory Profiling Framework. 449-473 - Haonan Li, Yu Hao, Yizhuo Zhai, Zhiyun Qian:
Enhancing Static Analysis for Practical Bug Detection: An LLM-Integrated Approach. 474-499 - Qian Chen, Chenyang Yu, Ruyan Liu, Chi Zhang, Yu Wang, Ke Wang, Ting Su, Linzhang Wang:
Evaluating the Effectiveness of Deep Learning Models for Foundational Program Analysis Tasks. 500-528 - Jonathan Castello, Patrick Redmond, Lindsey Kuper:
Inductive Diagrams for Causal Reasoning. 529-554 - Zikun Li, Jinjun Peng, Yixuan Mei, Sina Lin, Yi Wu, Oded Padon, Zhihao Jia:
Quarl: A Learning-Based Quantum Circuit Optimizer. 555-582 - Edward Lee, Yaoyu Zhao, Ondrej Lhoták, James You, Kavin Satheeskumar, Jonathan Immanuel Brachthäuser:
Qualifying System F<: Some Terms and Conditions May Apply. 583-612 - Tim Nelson, Ben Greenman, Siddhartha Prasad, Tristan Dyer, Ethan Bove, Qianfan Chen, Charles Cutting, Thomas Del Vecchio, Sidney Levine, Julianne Rudner, Ben Ryjikov, Alexander Varga, Andrew Wagner, Luke West, Shriram Krishnamurthi:
Forge: A Tool and Language for Teaching Formal Methods. 613-641 - Zhe Chen, Yunlong Zhu, Zhemin Wang:
Design and Implementation of an Aspect-Oriented C Programming Language. 642-669 - Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John H. Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells:
Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization. 670-697 - Anastasiya Kravchuk-Kirilyuk, Gary Feng, Jonas Iskander, Yizhou Zhang, Nada Amin:
Persimmon: Nested Family Polymorphism with Extensible Variant Types. 698-724 - Manasij Mukherjee, John Regehr:
Hydra: Generalizing Peephole Optimizations with Program Synthesis. 725-753 - Shigeyuki Sato, Tomoki Nakamaru:
Multiverse Notebook: Shifting Data Scientists to Time Travelers. 754-783 - Martin Avanzini, Gilles Barthe, Benjamin Grégoire, Georg Moser, Gabriele Vanoni:
Hopping Proofs of Expectation-Based Properties: Applications to Skiplists and Security Proofs. 784-809 - Gabriel Ryan, Burcu Cetin, Yongwhan Lim, Suman Jana:
Accurate Data Race Prediction in the Linux Kernel through Sparse Fourier Learning. 810-832 - Aaditya Naik, Adam Stein, Yinjun Wu, Mayur Naik, Eric Wong:
TorchQL: A Programming Framework for Integrity Constraints in Machine Learning. 833-863 - Olek Gierczak, Lucy Menon, Christos Dimoulas, Amal Ahmed:
Gradually Typed Languages Should Be Vigilant! 864-892 - Jesse Michel, Kevin Mu, Xuanda Yang, Sai Praveen Bangaru, Elias Rojas Collins, Gilbert Bernstein, Jonathan Ragan-Kelley, Michael Carbin, Tzu-Mao Li:
Distributions for Compositionally Differentiating Parametric Discontinuities. 893-922 - Lutz Klinkenberg, Christian Blumenthal, Mingshuai Chen, Darion Haase, Joost-Pieter Katoen:
Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. 923-953 - Yifan Zhang, Yuanfeng Shi, Xin Zhang:
Learning Abstraction Selection for Bayesian Program Analysis. 954-982 - David Binder, Ingo Skupin, Tim Süberkrüb, Klaus Ostermann:
Deriving Dependently-Typed OOP from First Principles. 983-1009 - Anan Kabaha, Dana Drachsler-Cohen:
Verification of Neural Networks' Global Robustness. 1010-1039 - Danielle Marshall, Dominic Orchard:
Functional Ownership through Fractional Uniqueness. 1040-1070 - Yang He, Pinhan Zhao, Xinyu Wang, Yuepeng Wang:
VeriEQL: Bounded Equivalence Verification for Complex SQL Queries with Integrity Constraints. 1071-1099 - Jialu Zhang, José Pablo Cambronero, Sumit Gulwani, Vu Le, Ruzica Piskac, Gustavo Soares, Gust Verbruggen:
PyDex: Repairing Bugs in Introductory Python Assignments using LLMs. 1100-1124 - Joanna C. S. Santos, Mehdi Mirakhorli, Ali Shokri:
Seneca: Taint-Based Call Graph Construction for Java Object Deserialization. 1125-1153 - Scott F. Smith, Robert Zhang:
A Pure Demand Operational Semantics with Applications to Program Analysis. 1154-1180 - Yichen Xu, Aleksander Boruch-Gruszecki, Martin Odersky:
Degrees of Separation: A Flexible Type System for Safe Concurrency. 1181-1207 - Mingwei Zheng, Qingkai Shi, Xuwei Liu, Xiangzhe Xu, Le Yu, Congyu Liu, Guannan Wei, Xiangyu Zhang:
ParDiff: Practical Static Differential Analysis of Network Protocol Parsers. 1208-1234 - Amanda Stjerna, Philipp Rümmer:
A Constraint Solving Approach to Parikh Images of Regular Languages. 1235-1263 - Zhaoyu Wang, Pingchuan Ma, Huaijin Wang, Shuai Wang:
PP-CSA: Practical Privacy-Preserving Software Call Stack Analysis. 1264-1293 - Constantin Enea, Eric Koskinen:
Scenario-Based Proofs for Concurrent Objects. 1294-1323 - Yongjian Li, Bohua Zhan, Jun Pang:
Mechanizing the CMP Abstraction for Parameterized Verification. 1324-1350 - Ryan Kavanagh, Brigitte Pientka:
Message-Observing Sessions. 1351-1379 - Yifei Lu, Weidong Hou, Minxue Pan, Xuandong Li, Zhendong Su:
Understanding and Finding Java Decompiler Bugs. 1380-1406 - Qianchuan Ye, Benjamin Delaware:
Taypsi: Static Enforcement of Privacy Policies for Policy-Agnostic Oblivious Computation. 1407-1436 - Pei Xu, Yuxiang Lei, Yulei Sui, Jingling Xue:
Iterative-Epoch Online Cycle Elimination for Context-Free Language Reachability. 1437-1462 - Abhishek Rose, Sorav Bansal:
Modeling Dynamic (De)Allocations of Local Memory for Translation Validation. 1463-1492
Volume 8, Number ICFP, 2024
ICFP 2024
- Jacques Carette, Chris Heunen, Robin Kaarsgaard, Amr Sabry:
How to Bake a Quantum Π. 1-29 - Li-yao Xia, Laura Israel, Maite Kramarz, Nicholas Coltharp, Koen Claessen, Stephanie Weirich, Yao Li:
Story of Your Lazy Function's Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy Programs. 30-63 - Michael Ballantyne, Mitch Gamburg, Jason Hemann:
Compiled, Extensible, Multi-language DSLs (Functional Pearl). 64-87 - Martin Elsman:
Double-Ended Bit-Stealing for Algebraic Data Types. 88-120 - Guillaume Melquiond, Josué Moreau:
A Safe Low-Level Language for Computer Algebra and Its Formally Verified Compiler. 121-146 - Paulo Henrique Torrens, Dominic Orchard, Cristiano D. Vasconcellos:
On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs. 147-176 - Manuel Serrano, Robert Bruce Findler:
The Functional, the Imperative, and the Sudoku: Getting Good, Bad, and Ugly to Get Along (Functional Pearl). 177-202 - Simon Oddershede Gregersen, Alejandro Aguirre, Philipp G. Haselwarter, Joseph Tassarotti, Lars Birkedal:
Almost-Sure Termination by Guarded Refinement. 203-233 - Atze Dijkstra, José Pedro Magalhães, Pierre Néron:
Functional Programming in Financial Markets (Experience Report). 234-248 - Yijia Chen, Lionel Parreaux:
The Long Way to Deforestation: A Type Inference and Elaboration Technique for Removing Intermediate Data Structures. 249-283 - Alejandro Aguirre, Philipp G. Haselwarter, Markus de Medeiros, Kwing Hei Li, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal:
Error Credits: Resourceful Reasoning about Error Bounds for Higher-Order Probabilistic Programs. 284-316 - Niek Mulleners, Johan Jeuring, Bastiaan Heeren:
Example-Based Reasoning about the Realizability of Polymorphic Programs. 317-337 - Clément Allain, Basile Clément, Alexandre Moine, Gabriel Scherer:
Snapshottable Stores. 338-369 - Patrick Bahr, Graham Hutton:
Beyond Trees: Calculating Graph-Based Compilers (Functional Pearl). 370-394 - David Binder, Marco Tzschentke, Marius Müller, Klaus Ostermann:
Grokking the Sequent Calculus (Functional Pearl). 395-425 - Son Ho, Aymeric Fromherz, Jonathan Protzenko:
Sound Borrow-Checking for Rust via Symbolic Semantics. 426-454 - Takuma Yoshioka, Taro Sekiyama, Atsushi Igarashi:
Abstracting Effect Systems for Algebraic Effect Handlers. 455-484 - Anton Lorenzen, Leo White, Stephen Dolan, Richard A. Eisenberg, Sam Lindley:
Oxidizing OCaml with Modal Memory Management. 485-514 - Bram Vandenbogaerde, Quentin Stiévenart, Coen De Roover:
Blame-Correct Support for Receiver Properties in Recursively-Structured Actor Contracts. 515-543 - Mara Malewski, Kenji Maillard, Nicolas Tabareau, Éric Tanter:
Gradual Indexed Inductive Types. 544-572 - Youngju Song, Dongjae Lee:
Refinement Composition Logic. 573-601 - Sébastien Michelland, Yannick Zakowski, Laure Gonnord:
Abstract Interpreters: A Monadic Approach to Modular Verification. 602-629 - Théo Winterhalter:
Dependent Ghosts Have a Reflection for Free. 630-658 - András Kovács:
Closure-Free Functional Programming in a Two-Level Type Theory. 659-692 - Tsung-Ju Chiang, Jeremy Yallop, Leo White, Ningning Xie:
Staged Compilation with Module Functors. 693-727 - Benjamin Quiring, David Van Horn:
Deriving with Derivatives: Optimizing Incremental Fixpoints for Higher-Order Flow Analysis. 728-755 - Ningning Xie, Daniel D. Johnson, Dougal Maclaurin, Adam Paszke:
Parallel Algebraic Effect Handlers. 756-788 - Calvin Beck, Irene Yoon, Hanxi Chen, Yannick Zakowski, Steve Zdancewic:
A Two-Phase Infinite/Finite Low-Level Memory Model: Reconciling Integer-Pointer Casts, Finite Space, and undef at the LLVM IR Level of Abstraction. 789-817 - Cole Kurashige, Ruyi Ji, Aditya Giridharan, Mark Barbone, Daniel Noor, Shachar Itzhaky, Ranjit Jhala, Nadia Polikarpova:
CCLemma: E-Graph Guided Lemma Discovery for Inductive Equational Proofs. 818-844 - Paul Downen:
Call-by-Unboxed-Value. 845-879 - Xu Xue, Bruno C. d. S. Oliveira:
Contextual Typing. 880-908 - Yahui Song, Darius Foo, Wei-Ngan Chin:
Specification and Verification for Unrestricted Algebraic Effects and Handling. 909-937 - Jiawei Chen, José Luiz Vargas de Mendonça, Bereket Ayele, Bereket Ngussie Bekele, Shayan Jalili, Pranjal Sharma, Nicholas Wohlfeil, Yicheng Zhang, Jean-Baptiste Jeannin:
Synchronous Programming with Refinement Types. 938-972 - Satoshi Kura, Hiroshi Unno:
Automated Verification of Higher-Order Probabilistic Programs via a Dependent Refinement Type System. 973-1002 - Noé De Santo, Aurèle Barrière, Clément Pit-Claudel:
A Coq Mechanization of JavaScript Regular Expression Semantics. 1003-1031
Volume 8, Number OOPSLA2, 2024
OOPSLA 2024 - Part 2
- Yichuan Li, Wei Song, Jeff Huang:
VarLifter: Recovering Variables and Types from Bytecode of Solidity Smart Contracts. 1-29 - Julien Simonnet, Matthieu Lemerre, Mihaela Sighireanu:
A Dependent Nominal Physical Type System for Static Analysis of Memory in Low Level Code. 30-59 - David Klopp, Sebastian Erdweg, André Pacak:
Object-Oriented Fixpoint Programming with Datalog. 60-86 - Zachary Palmer, Nathaniel Wesley Filardo, Ke Wu:
Intensional Functions. 87-112 - Shaan Nagy, Jinwoo Kim, Thomas W. Reps, Loris D'Antoni:
Automating Unrealizability Logic: Hoare-Style Proof Synthesis for Infinite Sets of Programs. 113-139 - Chan Gu Kang, Joonghoon Lee, Hakjoo Oh:
Statistical Testing of Quantum Programs via Fixed-Point Amplitude Amplification. 140-164 - William J. Bowman:
A Low-Level Look at A-Normal Form. 165-191 - Litao Zhou, Qianyong Wan, Bruno C. d. S. Oliveira:
Full Iso-Recursive Types. 192-221 - Chengyu Zhang, Zhendong Su:
SMT2Test: From SMT Formulas to Effective Test Cases. 222-245 - Azalea Raad, Julien Vanegue, Peter W. O'Hearn:
Non-termination Proving at Scale. 246-274 - Peiming Liu, Alexander J. Root, Anlun Xu, Yinying Li, Fredrik Kjolstad, Aart J. C. Bik:
Compiler Support for Sparse Tensor Convolutions. 275-303 - Maxime Legoupil, June Rousseau, Aïna Linn Georges, Jean Pichon-Pharabod, Lars Birkedal:
Iris-MSWasm: Elucidating and Mechanising the Security Invariants of Memory-Safe WebAssembly. 304-332 - Jos Craaijo, Freek Verbeek, Binoy Ravindran:
libLISA: Instruction Discovery and Analysis on x86-64. 333-361 - Jiangyi Liu, Charlie Murphy, Anvay Grover, Keith J. C. Johnson, Thomas W. Reps, Loris D'Antoni:
Synthesizing Formal Semantics from Executable Interpreters. 362-388 - Vineet Rajani, Gilles Barthe, Deepak Garg:
A Modal Type Theory of Expected Cost in Higher-Order Probabilistic Programs. 389-414 - Elisabet Lobo Vesga, Alejandro Russo, Marco Gaboardi, Carlos Tomé Cortiñas:
Sensitivity by Parametricity. 415-441 - Luke Geeson, James Brotherston, Wilco Dijkstra, Alastair F. Donaldson, Lee Smith, Tyler Sorensen, John Wickerson:
Mix Testing: Specifying and Testing ABI Compatibility of C/C++ Atomics Implementations. 442-467 - Andrew Blinn, Xiang Li, June Hyung Kim, Cyrus Omar:
Statically Contextualizing Large Language Models with Typed Holes. 468-498 - Zhengyao Lin, Joshua Gancher, Bryan Parno:
FlowCert: Translation Validation for Asynchronous Dataflow via Dynamic Fractional Permissions. 499-526 - Adhitha Dias, Logan Anderson, Kirshanthan Sundararajah, Artem Pelenitsyn, Milind Kulkarni:
SparseAuto: An Auto-scheduler for Sparse Tensor Computations using Recursive Loop Nest Restructuring. 527-556 - Seungmin Jeon, Kyeongmin Cho, Chan Gu Kang, Janggun Lee, Hakjoo Oh, Jeehoon Kang:
Quantum Probabilistic Model Checking for Time-Bounded Properties. 557-587 - Thomas Somers, Robbert Krebbers:
Verified Lock-Free Session Channels with Linking. 588-617 - Yoshiki Takashima, Chanhee Cho, Ruben Martins, Limin Jia, Corina S. Pasareanu:
Crabtree: Rust API Test Synthesis Guided by Coverage and Type. 618-647 - Wenjia Ye, Bruno C. d. S. Oliveira, Matías Toro:
Merging Gradual Typing. 648-676 - Federico Cassano, John Gouwar, Francesca Lucchetti, Claire Schlesinger, Anders Freeman, Carolyn Jane Anderson, Molly Q. Feldman, Michael Greenberg, Abhinav Jangda, Arjun Guha:
Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMs. 677-708 - Chenyuan Yang, Yinlin Deng, Runyu Lu, Jiayi Yao, Jiawei Liu, Reyhaneh Jabbarvand, Lingming Zhang:
WhiteFox: White-Box Compiler Fuzzing Empowered by Large Language Models. 709-735 - Michael Jungmair, Alexis Engelke, Jana Giceva:
HiPy: Extracting High-Level Semantics from Python Code for Data Processing. 736-762 - Loris D'Antoni, Shuo Ding, Amit Goel, Mathangi Ramesh, Neha Rungta, Chungha Sung:
Automatically Reducing Privilege for Access Control Policies. 763-790 - Ziteng Yang, Jun Shirako, Vivek Sarkar:
Fully Verified Instruction Scheduling. 791-816 - Linpeng Zhang, Noam Zilberstein, Benjamin Lucien Kaminski, Alexandra Silva:
Quantitative Weakest Hyper Pre: Unifying Correctness and Incorrectness Hyperproperties via Predicate Transformers. 817-845 - Ethan Chen, Jiwon Chang, Yuhao Zhu:
CoolerSpace: A Language for Physically Correct and Computationally Efficient Color Programming. 846-875 - Si Liu, Long Gu, Hengfeng Wei, David A. Basin:
Plume: Efficient and Complete Black-Box Checking of Weak Isolation Levels. 876-904 - Eric Hayden Campbell, Hossein Hojjat, Nate Foster:
Computing Precise Control Interface Specifications. 905-934 - Keith J. C. Johnson, Rahul Krishnan, Thomas W. Reps, Loris D'Antoni:
Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with Monotonic Semantics. 935-961 - Robin Webbers, Klaus von Gleissenthall, Ranjit Jhala:
Refinement Type Refutations. 962-987 - Luyu Cheng, Lionel Parreaux:
The Ultimate Conditional Syntax. 988-1017 - Paul Maximilian Bittner, Alexander Schultheiß, Benjamin Moosherr, Jeffrey M. Young, Leopoldo Teixeira, Eric Walkingshaw, Parisa Ataei, Thomas Thüm:
On the Expressive Power of Languages for Static Variability. 1018-1050 - Long Pham, Di Wang, Feras A. Saad, Jan Hoffmann:
Programmable MCMC with Soundly Composed Guide Programs. 1051-1080 - Paulo Emílio de Vilhena, Ori Lahav, Viktor Vafeiadis, Azalea Raad:
Extending the C/C++ Memory Model with Inline Assembly. 1081-1107 - Cassia Torczon, Emmanuel Suárez Acevedo, Shubh Agrawal, Joey Velez-Ginorio, Stephanie Weirich:
Effects and Coeffects in Call-by-Push-Value. 1108-1134 - Aleksander Boruch-Gruszecki, Adrien Ghosn, Mathias Payer, Clément Pit-Claudel:
Gradient: Gradual Compartmentalization via Object Capabilities Tracked in Types. 1135-1161 - Alexander J. Root, Bobby Yan, Peiming Liu, Christophe Gyurgyik, Aart J. C. Bik, Fredrik Kjolstad:
Compilation of Shape Operators on Sparse Arrays. 1162-1188 - Philipp G. Haselwarter, Kwing Hei Li, Markus de Medeiros, Simon Oddershede Gregersen, Alejandro Aguirre, Joseph Tassarotti, Lars Birkedal:
Tachis: Higher-Order Separation Logic with Credits for Expected Costs. 1189-1218 - Aaron Bembenek, Michael Greenberg, Stephen Chong:
Making Formulog Fast: An Argument for Unconventional Datalog Evaluation. 1219-1248 - Andrew Wagner, Zachary Eisbach, Amal Ahmed:
Realistic Realizability: Specifying ABIs You Can Count On. 1249-1278 - Thibault Dardinier, Anqi Li, Peter Müller:
Hypra: A Deductive Program Verifier for Hyper Hoare Logic. 1279-1308 - Chijin Zhou, Bingzhou Qian, Gwihwan Go, Quan Zhang, Shanshan Li, Yu Jiang:
PolyJuice: Detecting Mis-compilation Bugs in Tensor Compilers with Equality Saturation Based Rewriting. 1309-1335 - Zhichao Guan, Yiyuan Cao, Tailai Yu, Ziheng Wang, Di Wang, Zhenjiang Hu:
Semantics Lifting for Syntactic Sugar. 1336-1361 - Boyao Ding, Qingwei Li, Yu Zhang, Fugen Tang, Jinbao Chen:
MEA2: A Lightweight Field-Sensitive Escape Analysis with Points-to Calculation for Golang. 1362-1389 - Meghana Sistla, Swarat Chaudhuri, Thomas W. Reps:
Weighted Context-Free-Language Ordered Binary Decision Diagrams. 1390-1419 - Arthur Correnson, Tobias Nießen, Bernd Finkbeiner, Georg Weissenbacher:
Finding ∀∃ Hyperbugs using Symbolic Execution. 1420-1445 - Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers:
Multris: Functional Verification of Multiparty Message Passing in Separation Logic. 1446-1474 - Hannes Saffrich, Yuki Nishida, Peter Thiemann:
Law and Order for Typestate with Borrowing. 1475-1503 - Xin Yi, Hengbiao Yu, Liqian Chen, Xiaoguang Mao, Ji Wang:
FPCC: Detecting Floating-Point Errors via Chain Conditions. 1504-1531 - Zhenyu Yan, Xin Zhang, Peng Di:
Scaling Abstraction Refinement for Program Analyses in Datalog using Graph Neural Networks. 1532-1560 - Zhengyang Liu, Stefan Mada, John Regehr:
Minotaur: A SIMD-Oriented Synthesizing Superoptimizer. 1561-1585 - David Klopp, Sebastian Erdweg, André Pacak:
A Typed Multi-level Datalog IR and Its Compiler Framework. 1586-1614 - Yiyu Zhang, Tianyi Liu, Yueyang Wang, Yun Qi, Kai Ji, Jian Tang, Xiaoliang Wang, Xuandong Li, Zhiqiang Zuo:
HardTaint: Production-Run Dynamic Taint Analysis via Selective Hardware Tracing. 1615-1640 - David Schwartz, Ankith Kowshik, Luís Pina:
Jmvx: Fast Multi-threaded Multi-version Execution and Record-Replay for Managed Languages. 1641-1669 - Cong Ma, Zhaoyi Ge, Edward Lee, Yizhou Zhang:
Lexical Effect Handlers, Directly. 1670-1698 - Alexis Le Glaunec, Lingkun Kong, Konstantinos Mamouras:
HybridSA: GPU Acceleration of Multi-pattern Regex Matching using Bit Parallelism. 1699-1728 - Jeff Eymer, Philip Dexter, Joseph Raskind, Yu David Liu:
A Runtime System for Interruptible Query Processing: When Incremental Computing Meets Fine-Grained Parallelism. 1729-1756 - Antonin Reitz, Aymeric Fromherz, Jonathan Protzenko:
StarMalloc: Verifying a Modern, Hardened Memory Allocator. 1757-1786 - Robert Schenck, Nikolaj Hey Hinnerskov, Troels Henriksen, Magnus Madsen, Martin Elsman:
AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming. 1787-1813 - Callista Le, Kiran Gopinathan, Koon Wen Lee, Seth Gilbert, Ilya Sergey:
Concurrent Data Structures Made Easy. 1814-1842 - Ningke Li, Yuekang Li, Yi Liu, Ling Shi, Kailong Wang, Haoyu Wang:
Drowzee: Metamorphic Testing for Fact-Conflicting Hallucination Detection in Large Language Models. 1843-1872 - Nikhil Pimpalkhare, Zachary Kincaid:
Monotone Procedure Summarization via Vector Addition Systems and Inductive Potentials. 1873-1899 - Constantin Enea, Dimitra Giannakopoulou, Michalis Kokologiannakis, Rupak Majumdar:
Model Checking Distributed Protocols in Must. 1900-1927 - Andrea Borgarelli, Constantin Enea, Rupak Majumdar, Srinidhi Nagendra:
Reward Augmentation in Reinforcement Learning for Testing Distributed Systems. 1928-1954 - Qian Wang, Ralf Jung:
Rustlantis: Randomized Differential Testing of the Rust Compiler. 1955-1981 - Guillaume Ambal, Brijesh Dongol, Haggai Eran, Vasileios Klimis, Ori Lahav, Azalea Raad:
Semantics of Remote Direct Memory Access: Operational and Declarative Models of RDMA on TSO Architectures. 1982-2009 - Wenjia Ye, Yaozhu Sun, Bruno C. d. S. Oliveira:
Imperative Compositional Programming: Type Sound Distributive Intersection Subtyping with References via Bidirectional Typing. 2010-2039 - Jifeng Wu, Caroline Lemieux:
QuAC: Quick Attribute-Centric Type Inference for Python. 2040-2069 - Georgian-Vlad Saioc, Julien Lange, Anders Møller:
Automated Verification of Parametric Channel-Based Process Communication. 2070-2096 - Hristo Venev, Timon Gehr, Dimitar Dimitrov, Martin T. Vechev:
Modular Synthesis of Efficient Quantum Uncomputation. 2097-2124 - Denis Carnier, François Pottier, Steven Keuchel:
Type Inference Logics. 2125-2155 - Doehyun Baek, Jakob Getz, Yusung Sim, Daniel Lehmann, Ben L. Titzer, Sukyoung Ryu, Michael Pradel:
Wasm-R3: Record-Reduce-Replay for Realistic and Standalone WebAssembly Benchmarks. 2156-2182 - Kelvin Qian, Scott F. Smith, Brandon Stride, Shiwei Weng, Ke Wu:
Semantic-Type-Guided Bug Finding. 2183-2210 - Benjamin Mariano, Ziteng Wang, Shankara Pailoor, Christian S. Collberg, Isil Dillig:
Control-Flow Deobfuscation using Trace-Informed Compositional Program Synthesis. 2211-2241 - Caleb Kim, Pai Li, Anshuman Mohan, Andrew Butt, Adrian Sampson, Rachit Nigam:
Unifying Static and Dynamic Intermediate Languages for Accelerator Generators. 2242-2267 - Jonas Norlinder, Erik Österlund, David Black-Schaffer, Tobias Wrigstad:
Mark-Scavenge: Waiting for Trash to Take Itself Out. 2268-2295 - Arthur Oliveira Vale, Zhongye Wang, Yixuan Chen, Peixin You, Zhong Shao:
Compositionality and Observational Refinement for Linearizability with Crashes. 2296-2324 - Augustine Wong, Paul Bucci, Ivan Beschastnikh, Alexandra Fedorova:
Making Sense of Multi-threaded Application Performance at Scale with NonSequitur. 2325-2354 - Chen Yang, Junjie Chen, Jiajun Jiang, Yuliang Huang:
Dependency-Aware Code Naturalness. 2355-2377 - Dominik Winterer, Zhendong Su:
Validating SMT Solvers for Correctness and Performance via Grammar-Based Enumeration. 2378-2401 - Shelly Grossman, John Toman, Alexander Bakst, Sameer Arora, Mooly Sagiv, Chandrakana Nandi:
Practical Verification of Smart Contracts using Memory Splitting. 2402-2433 - Dennis Liew, Tiago Cogumbreiro, Julien Lange:
Sound and Partially-Complete Static Analysis of Data-Races in GPU Programs. 2434-2461 - Mario Alvarez-Picallo, Teodoro Freund, Dan R. Ghica, Sam Lindley:
Effect Handlers for C via Coroutines. 2462-2489 - Georgios-Petros Drosos, Thodoris Sotiropoulos, Georgios Alexopoulos, Dimitris Mitropoulos, Zhendong Su:
When Your Infrastructure Is a Buggy Program: Understanding Faults in Infrastructure as Code Ecosystems. 2490-2520 - Jinhao Tan, Bruno C. d. S. Oliveira:
A Case for First-Class Environments. 2521-2550 - Amir Kafshdar Goharshady, Chun Kit Lam, Lionel Parreaux:
Fast and Optimal Extraction for Sparse Equality Graphs. 2551-2577 - Kartik Nagar, Anmol Sahoo, Romit Roy Chowdhury, Suresh Jagannathan:
Automated Robustness Verification of Concurrent Data Structure Libraries against Relaxed Memory Models. 2578-2605 - Shashin Halalingaiah, Vijay Sundaresan, Daryl Maier, V. Krishna Nandivada:
The ART of Sharing Points-to Analysis: Reusing Points-to Analysis Results Safely and Efficiently. 2606-2632 - Haofeng Li, Chenghang Shi, Jie Lu, Lian Li, Jingling Xue:
Boosting the Performance of Alias-Aware IFDS Analysis with CFL-Based Environment Transformers. 2633-2661 - Taro Sekiyama, Hiroshi Unno:
Higher-Order Model Checking of Effect-Handling Programs with Answer-Type Modification. 2662-2691
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
last updated on 2026-09-01 03:22 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint
dblp was originally created in 1993 at:
since 2018, dblp has been operated, funded, and maintained by:
Schloss Dagstuhl - Leibniz Center for Informatics is a member of the Leibniz Association and is funded by the federal government of Germany and the states of Germany, especially Saarland and Rhineland‑Palatinate.
