default search action
Proceedings of the ACM on Programming Languages, Volume 7
Volume 7, Number POPL, January 2023
- Christopher Pulte
, Dhruv C. Makwana
CN: Verifying Systems C Code with Separation-Logic Refinement Types. 1-32 - Alejandro Aguirre
Step-Indexed Logical Relations for Countable Nondeterminism and Probabilistic Choice. 33-60 - Pedro Abreu
A Type-Based Approach to Divide-and-Conquer Recursion in Coq. 61-90 - Yanjun Wang
Comparative Synthesis: Learning Near-Optimal Network Designs by Query. 91-120 - Alexander K. Lew
ADEV: Sound Automatic Differentiation of Expected Values of Probabilistic Programs. 121-153 - Naoki Kobayashi
HFL(Z) Validity Checking for Automated Program Verification. 154-184 - Aaron Bembenek
From SMT to ASP: Solver-Based Approaches to Solving Datalog Synthesis-as-Rule-Selection Problems. 185-217 - Axel Kerinec
Why Are Proofs Relevant in Proof-Relevant Models? 218-248 - Aurèle Barrière
Formally Verified Native Code Generation in an Effectful JIT: Turning the CompCert Backend into a Formally Verified JIT Compiler. 249-277 - Joel D. Day
On the Expressive Power of String Constraints. 278-308 - Peng Fu
Proto-Quipper with Dynamic Lifting. 309-334 - Wonyeol Lee
Smoothness Analysis for Probabilistic Programs with Application to Optimised Variational Inference. 335-366 - Konstantinos Kallas
Executing Microservice Applications on Serverless, Correctly. 367-395 - David Cao
babble: Learning Better Abstractions with E-Graphs and Anti-unification. 396-424 - Alexandra E. Michael
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code. 425-454 - Sirui Lu
Grisette: Symbolic Compilation as a Functional Programming Library. 455-487 - Andrew M. Pitts
Locally Nameless Sets. 488-514 - Nick Rioux
A Bowtie for a Beast: Overloading, Eta Expansion, and Extensible Data Types in F⋈. 515-543 - Michalis Kokologiannakis
Kater: Automating Weak Memory Model Metatheory and Consistency Checking. 544-572 - Timos Antonopoulos
An Algebra of Alignment for Relational Verification. 573-603 - Yu Gu
Optimal CHC Solving via Termination Proofs. 604-631 - Sergey Goncharov
Towards a Higher-Order Mathematical Operational Semantics. 632-658 - Jinwoo Kim
Unrealizability Logic. 659-688 - Simon Castellan
The Geometry of Causality: Multi-token Geometry of Interaction and Its Causal Unfolding. 689-717 - Alexandre Moine
A High-Level Separation Logic for Heap Space under Garbage Collection. 718-747 - Emanuele D'Osualdo
The Path to Durable Linearizability. 748-774 - Michael Sammler
DimSum: A Decentralized Approach to Multi-language Semantics and Verification. 775-805 - Emmanuel Hainry
A General Noninterference Policy for Polynomial Time. 806-832 - Li Zhou
CoqQ: Foundational Verification of Quantum Programs. 833-865 - Joshua Gancher
A Core Calculus for Equational Proofs of Cryptographic Protocols. 866-892 - Han Xu
Making a Type Difference: Subtraction on Intersection Types as Generalized Record Operations. 893-920 - Finn Voichick
Qunity: A Unified Language for Quantum and Classical Computing. 921-951 - José Cambronero
FlashFill++: Scaling Programming by Example by Cutting to the Chase. 952-981 - Shuo Ding
Witnessability of Undecidable Problems. 982-1002 - Yuanbo Li
Single-Source-Single-Target Interleaved-Dyck Reachability via Integer Linear Programming. 1003-1026 - Jules Jacobs
Higher-Order Leak and Deadlock Free Locks. 1027-1057 - Rajeev Alur
A Robust Theory of Series Parallel Graphs. 1058-1088 - Arthur Oliveira Vale
A Compositional Theory of Linearizability. 1089-1120 - Youngju Song
Conditional Contextual Refinement. 1121-1151 - Daan Leijen
Tail Recursion Modulo Context: An Equational Approach. 1152-1181 - Matthew Bowers
Top-Down Synthesis for Library Learning. 1182-1213 - Andrei Popescu
Admissible Types-to-PERs Relativization in Higher-Order Logic. 1214-1245 - Alexey Radul
You Only Linearize Once: Tangents Transpose to Gradients. 1246-1274 - Zachary Kincaid
When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic. 1275-1307 - Mosaad Al Thokair
Dynamic Race Detection with O(1) Samples. 1308-1337 - Swaraj Dash
Affine Monads and Lazy Structures for Bayesian Programming. 1338-1368 - Zilin Chen
Dargent: A Silver Bullet for Verified Data Layout Refinement. 1369-1395 - Litao Zhou
Recursive Subtyping for All. 1396-1425 - Azadeh Farzan
Stratified Commutativity in Verification Algorithms for Concurrent Programs. 1426-1453 - Jianlin Li
Type-Preserving, Dependence-Aware Guide Generation for Sound, Effective Amortized Probabilistic Inference. 1454-1482 - Victor Arrial
Quantitative Inhabitation for Different Lambda Calculi in a Unifying Framework. 1483-1513 - Jules Jacobs
Fast Coalgebraic Bisimilarity Minimization. 1514-1541 - Abhishek Kr Singh
An Operational Approach to Library Abstraction under Relaxed Memory Concurrency. 1542-1572 - Tom Smeding
Efficient Dual-Numbers Reverse AD via Well-Known Program Transformations. 1573-1600 - Cinzia Di Giusto
A Partial Order View of Message-Passing Communication Models. 1601-1627 - Ria Das
Combining Functional and Automata Synthesis to Discover Causal Reactive Programs. 1628-1658 - Kuen-Bang Hou (Favonia)
An Order-Theoretic Analysis of Universe Polymorphism. 1659-1685 - Viktor Palmkvist
Statically Resolvable Ambiguity. 1686-1712 - Paraschos Koutris
The Fine-Grained Complexity of CFL Reachability. 1713-1739 - Vasileios Klimis
Taking Back Control in an Intermediate Representation for GPU Computing. 1740-1769 - Nicolas Chappe
Choice Trees: Representing Nondeterministic, Recursive, and Impure Programs in Coq. 1770-1800 - Casper Bach Poulsen
Hefty Algebras: Modular Elaboration of Higher-Order Algebraic Effects. 1801-1831 - Francesco Gavazzo
Elements of Quantitative Rewriting. 1832-1863 - Filippo Bonchi
Deconstructing the Calculus of Relations with Tape Diagrams. 1864-1894 - Matthieu Lemerre
SSA Translation Is an Abstract Interpretation. 1895-1924 - Ankush Das
Probabilistic Resource-Aware Session Types. 1925-1956 - Kevin Batz
A Calculus for Amortized Expected Runtimes. 1957-1986 - Sebastian Hunt
Reconciling Shannon and Scott with a Lattice of Computable Information. 1987-2016 - Jerome Jochems
Higher-Order MSL Horn Constraints. 2017-2047 - Woosuk Lee
Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive Expressions. 2048-2078 - Taro Sekiyama
Temporal Verification with Answer-Effect Modification: Dependent Temporal Type-and-Effect System with Delimited Continuations. 2079-2110 - Hiroshi Unno
Modular Primal-Dual Fixpoint Logic Solving for Temporal Verification. 2111-2140 - Pascal Baumann
Context-Bounded Verification of Context-Free Specifications. 2141-2170 - Loïc Pujet
Impredicative Observational Equality. 2171-2196
Volume 7, Number OOPSLA1, April 2023
- Shaohua Li
Accelerating Fuzzing through Prefix-Guided Execution. 1-27 - Chenglin Wang
Solving Conditional Linear Recurrences for Program Verification: The Periodic Case. 28-55 - Zhengyao Lin
Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier. 56-84 - Shraddha Barke
Grounded Copilot: How Programmers Interact with Code-Generating Models. 85-111 - Lorenzo Gheri
Hybrid Multiparty Session Types: Compositionality for Protocol Specification through Endpoint Projection. 112-142 - Paul Krogmeier
Languages with Decidable Learning: A Meta-theorem. 143-171 - Christopher Wagner
Enabling Bounded Verification of Doubly-Unbounded Distributed Agreement-Based Systems via Bounded Regions. 172-200 - Bo Wang
User-Customizable Transpilation of Scripting Languages. 201-229 - Xing Zhang
Bidirectional Object-Oriented Programming: Towards Programmatic and Direct Manipulation of Objects. 230-255 - Wenjia Ye
A Gradual Probabilistic Lambda Calculus. 256-285 - Andrea Lattuada
Verus: Verifying Rust Programs using Linear Ghost Types. 286-315 - Jie Zhou
Fat Pointers for Temporal Memory Safety of C. 316-347 - Chan Gu Kang
Modular Component-Based Quantum Circuit Synthesis. 348-375 - Anthony C. J. Fox
A Verification Methodology for the Arm® Confidential Computing Architecture: From a Secure Specification to Safe Implementations. 376-405 - Jan Menz
Compositional Security Definitions for Higher-Order Where Declassification. 406-433 - Yuval Shapira
Deep Learning Robustness Verification for Few-Pixel Attacks. 434-461 - Ike Mulder
Proof Automation for Linearizability in Separation Logic. 462-491 - Alexis Le Glaunec
Regular Expression Matching using Bit Vector Automata. 492-521 - Noam Zilberstein
Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. 522-550 - Mehmet Emre
Aliasing Limits on Translating C to Safe Rust. 551-579 - Guoqiang Zhang
Automated Translation of Functional Big Data Queries to SQL. 580-608 - Yongwei Yuan
Live Pattern Matching with Typed Holes. 609-635 - Zhenyang Xu
Pushing the Limit of 1-Minimality of Language-Agnostic Program Reduction. 636-664 - David Chiang
Exact Recursive Probabilistic Programming. 665-695 - Shenghua Feng
Lower Bounds for Possibly Divergent Probabilistic Programs. 696-726 - Amir Kafshdar Goharshady
Algebro-geometric Algorithms for Template-Based Synthesis of Polynomial Programs. 727-756 - Levin N. Winter
Randomized Testing of Byzantine Fault Tolerant Algorithms. 757-788 - Thibault Dardinier
Verification-Preserving Inlining in Automatic Separation Logic Verifiers. 789-818 - Ruyi Ji
Improving Oracle-Guided Inductive Synthesis by Efficient Question Selection. 819-847 - Marius Müller
Back to Direct Style: Typed and Tight. 848-875 - Ori Roth
Fluent APIs in Functional Languages. 876-901
Volume 7, Number PLDI, June 2023
- Alexander Bagnall
Formally Verified Samplers from Probabilistic Programs with Loops and Conditioning. 1-24 - Kiran Gopinathan
Mostly Automated Proof Repair for Verified Libraries. 25-49 - Timothy Alberdingk Thijm
Modular Control Plane Verification via Temporal Invariants. 50-75 - Dan Cascaval
A Lineage-Based Referencing DSL for Computer-Aided Design. 76-99 - Conrad Watt
WasmRef-Isabelle: A Verified Monadic Interpreter and Industrial Fuzzing Oracle for WebAssembly. 100-123 - Mohamed Tarek Ibn Ziad
cuCatch: A Debugging Tool for Efficiently Catching Memory Safety Violations in CUDA Applications. 124-147 - John M. Li
Lilac: A Modal Separation Logic for Conditional Probability. 148-171 - Fengjuan Gao
Discrete Adversarial Attack to Models of Code. 172-195 - Sunjae Park
HEaaN.MLIR: An Optimizing Compiler for Fast Ring-Based Homomorphic Encryption. 196-220 - Martin Elsman
Garbage-Collection Safety for Region-Based Type-Polymorphic Programs. 221-243 - Nikita Koval
CQS: A Formally-Verified Framework for Fair and Abortable Synchronization. 244-266 - Shamiek Mangipudi
Generalized Policy-Based Noninterference for Efficient Confidentiality-Preservation. 267-291 - Kyeongmin Cho
Memento: A Framework for Detectable Recoverability in Persistent Memory. 292-317 - Yuxiang Lei
Recursive State Machine Guided Graph Folding for Context-Free Language Reachability. 318-342 - Rachit Nigam
Modular Hardware Design with Timeline Types. 343-367 - Tony Nuda Zhang
Performal: Formal Verification of Latency Properties for Distributed Systems. 368-393 - Manya Bansal
Mosaic: An Interoperable Compiler for Tensor Algebra. 394-419 - Zachary D. Sisco
Loop Rerolling for Hardware Decompilation. 420-442 - Zhe Tao
Architecture-Preserving Provable Repair of Deep Neural Networks. 443-467 - Yihong Zhang
Better Together: Unifying Datalog and Equality Saturation. 468-492 - Jihyeok Park
Feature-Sensitive Coverage for Conformance Testing of Programming Language Implementations. 493-515 - Yulong Huang
Defunctionalization with Dependent Types. 516-538 - Wenjie Ma
Context Sensitivity without Contexts: A Cut-Shortcut Approach to Fast and Precise Pointer Analysis. 539-564 - Ahmed Bouajjani
Dynamic Partial Order Reduction for Checking Correctness against Transaction Isolation Levels. 565-590 - Tetsuro Yamazaki
Collecting Cyclic Garbage across Foreign Function Interfaces: Who Takes the Last Piece of Cake? 591-614 - Joseph Tassarotti
Verified Density Compilation for a Probabilistic Programming Language. 615-637 - Junrui Liu
Conflict-Driven Synthesis for Layout Engines. 638-659 - Lauren Pick
Psym: Efficient Symbolic Exploration of Distributed Systems. 660-685 - Celeste Barnaby
ImageEye: Batch Image Processing using Program Synthesis. 686-711 - Stefan K. Muller
Responsive Parallelism with Synchronization. 712-735 - Milijana Surbatovich
A Type System for Safe Intermittent Computing. 736-760 - Hünkar Can Tunç
Optimal Reads-From Consistency Checking for C11-Style Memory Models. 761-785 - Mark Niklas Müller
Abstract Interpretation of Fixpoint Iterators with Applications to Neural Networks. 786-810 - Dongjae Lee
Fair Operational Semantics. 811-834 - Amanda Xu
Synthesizing Quantum-Circuit Optimizers. 835-859 - Yongwei Yuan
Trace-Guided Inductive Synthesis of Recursive Functional Programs. 860-883 - Martin Elsman
Parallelism in a Region Inference Context. 884-906 - Raphael Isemann
Don't Look UB: Exposing Sanitizer-Eliding Compiler Optimizations. 907-927 - Dragana Milovancevic
Proving and Disproving Equivalence of Functional Programming Assignments. 928-951 - Hrutvik Kanabar
PureCake: A Verified Compiler for a Lazy Functional Language. 952-976 - William Brandon
Better Defunctionalization through Lambda Set Specialization. 977-1000 - Qianchuan Ye
Taype: A Policy-Agnostic Language for Oblivious Computation. 1001-1025 - Dan Moseley
Derivative Based Nonbacktracking Real-World Regex Matching with Backtracking Semantics. 1026-1049 - Martin Avanzini
Automated Expected Value Analysis of Recursive Programs. 1050-1072 - Jialun Zhang
Interval Parsing Grammars for File Format Parsing. 1073-1095 - Xiaojia Rao
Iris-Wasm: Robust and Modular Verification of WebAssembly Programs. 1096-1120 - Thomas Sewell
Cakes That Bake Cakes: Dynamic Computation in CakeML. 1121-1144 - Andrés Goens
Compound Memory Models. 1145-1168 - Scott Kovach
Indexed Streams: A Formal Intermediate Representation for Fused Contraction Programs. 1169-1193 - Jeremy Yallop
flap: A Deterministic Parser with Fused Lexing. 1194-1217 - Yu-Fang Chen
An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits. 1218-1243 - Zhe Zhou
Covering All the Bases: Type-Based Verification of Test Input Generators. 1244-1267 - Joel Kuepper
CryptOpt: Verified Compilation with Randomized Program Search for Cryptographic Primitives. 1268-1292 - Olivier Tardieu
Reliable Actors with Retry Orchestration. 1293-1316 - Mojtaba Valizadeh
Search-Based Regular Expression Inference on a GPU. 1317-1339 - Ike Mulder
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. 1340-1364 - George Zakhour
Type-Checking CRDT Convergence. 1365-1388 - Andreia Mordido
Parameterized Algebraic Protocols. 1389-1413 - Jonás Fiala
Leveraging Rust Types for Program Synthesis. 1414-1437 - Zongyuan Liu
VMSL: A Separation Logic for Mechanised Robust Safety of Virtual Machines Communicating above FF-A. 1438-1462 - Ziyang Li
Scallop: A Language for Neurosymbolic Programming. 1463-1487 - Seemanta Saha
Obtaining Information Leakage Bounds via Approximate Model Counting. 1488-1509 - Shankara Pailoor
Automated Detection of Under-Constrained Circuits in Zero-Knowledge Proofs. 1510-1532 - Nico Lehmann
Flux: Liquid Types for Rust. 1533-1557 - Jatin Arora
Efficient Parallel Functional Programming with Effects. 1558-1583 - Sankha Narayan Guria
Absynthe: Abstract Interpretation-Guided Synthesis. 1584-1607 - Ende Jin
Extensible Metatheory Mechanization via Family Polymorphism. 1608-1632 - Nariyoshi Chida
Repairing Regular Expressions for Extraction. 1633-1656 - Yongho Yoon
Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation. 1657-1681 - Marco Eilers
CommCSL: Proving Information Flow Security for Concurrent Programs using Abstract Commutativity. 1682-1707 - Alexander K. Lew
Probabilistic Programming with Stochastic Probabilities. 1708-1732 - Hünkar Can Tunç
Sound Dynamic Deadlock Prediction in Linear Time. 1733-1758 - Jacob Prinz
Merging Inductive Relations. 1759-1778 - Noah Bertram
Cutting the Cake: A Language for Fair Division. 1779-1800 - Bastien Lecoeur
Program Reconditioning: Avoiding Undefined Behaviour When Finding and Reducing Compiler Bugs. 1801-1825 - Vsevolod Livinskii
Fuzzing Loop Optimizations in Compilers for C++ and Data-Parallel Languages. 1826-1847 - Roland Meyer
Embedding Hindsight Reasoning in Separation Logic. 1848-1871 - Sung-Hwan Lee
Putting Weak Memory in Order via a Promising Intermediate Representation. 1872-1895 - Jingbo Wang
Synthesizing MILP Constraints for Efficient and Robust Optimization. 1896-1919 - Shubham Ugare
Incremental Verification of Neural Networks. 1920-1945 - Luca Beurer-Kellner
Prompting Is Programming: A Query Language for Large Language Models. 1946-1969 - Tom Yuviler
One Pixel Adversarial Attacks via Sketched Programs. 1970-1994 - Lucas Wilkinson
Register Tiling for Unstructured Sparsity in Neural Network Inference. 1995-2020
Volume 7, Number ICFP, August 2023
- Kazutaka Matsuda
Embedding by Unembedding. 1-47 - Hiroyuki Katsura
Higher-Order Property-Directed Reachability. 48-77 - Simon Fowler
Special Delivery: Programming with Mailbox Types. 78-107 - Thomas Bourgeat
Flexible Instruction-Set Semantics via Abstract Monads (Experience Report). 108-124 - Mahsa Varshosaz
Formal Specification and Testing for Reinforcement Learning. 125-158 - Lukas Lazarek
How to Evaluate Blame for Gradual Types, Part 2. 159-186 - Jad Elkhaleq Ghalayini
Explicit Refinement Types. 187-214 - Giuseppe Castagna
Typing Records, Maps, and Structs. 215-258 - Nada Amin
LURK: Lambda, the Ultimate Recursive Knowledge (Experience Report). 259-274 - Anton Lorenzen
FP²: Fully in-Place Functional Programming. 275-304 - Ryan G. Scott
Trustworthy Runtime Verification via Bisimulation (Experience Report). 305-321 - Harrison Goldstein
Reflecting on Random Generation. 322-355 - Alex Hubers
Generic Programming with Extensible Data Types: Or, Making Ad Hoc Extensible Data Types Less Ad Hoc. 356-384 - Son Ho
Modularity, Code Specialization, and Zero-Cost Abstractions for Program Verification. 385-416 - Lennart Augustsson
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. 417-447 - Matthew Lutze
With or Without You: Programming with Effect Exclusion. 448-475 - Patrick Bahr
Asynchronous Modal FRP. 476-510 - Filip Sieczkowski
A General Fine-Grained Reduction Theory for Effect Handlers. 511-540 - Gan Shen
HasChor: Functional Choreographic Programming for All (Functional Pearl). 541-565 - Zhixuan Yang
Modular Models of Monoids with Operations. 566-603 - Ningning Xie
MacoCaml: Staging Composable and Compilable Macros. 604-648 - Yiyun Liu
Dependently-Typed Programming with Logical Equality Reflection. 649-685 - Joachim Breitner
More Fixpoints! (Functional Pearl). 686-710 - Peter Thiemann
Intrinsically Typed Sessions with Callbacks (Functional Pearl). 711-739 - Patrick Bahr
Calculating Compilers for Concurrency. 740-767 - Jules Jacobs
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). 768-795 - Kuang-Chen Lu
What Happens When Students Switch (Functional) Languages (Experience Report). 796-812 - Thaïs Baudon
Bit-Stealing Made Legal: Compilation for Custom Memory Representations of Algebraic Data Types. 813-846 - Léon Gondelman
Verifying Reliable Network Components in a Distributed Separation Logic with Dependent Separation Protocols. 847-877 - Jessica Shi
Etna: An Evaluation Platform for Property-Based Testing (Experience Report). 878-894 - Conal Elliott
Timely Computation. 895-919 - Andreas Abel
A Graded Modal Dependent Type Theory with a Universe and Erasure, Formalized. 920-954 - Sven Keidel
Combinator-Based Fixpoint Algorithms for Big-Step Abstract Interpreters. 955-981
Volume 7, Number OOPSLA2, October 2023
- Pu (Luke) Yi
Hardware-Aware Static Optimization of Hyperdimensional Computations. 1-30 - Travis Hance
Leaf: Modularity for Temporary Sharing in Separation Logic. 31-58 - Léo Gourdin
Formally Verifying Optimizations with Block Simulations. 59-88 - Yican Sun
Synthesizing Efficient Memoization Algorithms. 89-115 - Hervé Paulino
AtomiS: Data-Centric Synchronization Made Practical. 116-145 - Thierry Renaux
Secure RDTs: Enforcing Access Control Policies for Offline Available JSON Data. 146-172 - Girish Mururu
Beacons: An End-to-End Compiler Framework for Predicting and Utilizing Dynamic Loop Characteristics. 173-203 - Mahdi Ghorbani
Compiling Structured Tensor Algebra. 204-233 - Qinlin Chen
The Essence of Verilog: A Tractable and Tested Operational Semantics for Verilog. 234-263 - Chengcheng Wan
Run-Time Prevention of Software Integration Failures of Machine Learning APIs. 264-291 - Giovanna Kobus Conrado
The Bounded Pathwidth of Control-Flow Graphs. 292-317 - Octave Larose
AST vs. Bytecode: Interpreters in the Age of Meta-Compilation. 318-346 - Andreas Rossberg
Mutually Iso-Recursive Subtyping. 347-373 - Chuta Sano
Mechanizing Session-Types using a Structural View: Enforcing Linearity without Linearity. 374-399 - Oliver Bracevac
Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect Dependencies. 400-430 - Ishan Bhanuka
Getting into the Flow: Towards Better Type Error Messages for Constraint-Based Type Inference. 431-459 - Luna Phipps-Costin
Continuing WebAssembly with Effect Handlers. 460-485 - Shangwen Wang
Two Birds with One Stone: Boosting Code Generation and Code Search via a Generative Adversarial Network. 486-515 - Magnus Madsen
Fast and Efficient Boolean Unification for Hindley-Milner-Style Type and Effect Systems. 516-543 - Ben Greenman
How Profilers Can Help Navigate Type Migration. 544-573 - Matthew Flatt
Rhombus: A New Spin on Macros without All the Parentheses. 574-603 - Chijin Zhou
Towards Better Semantics Exploration for Browser Fuzzing. 604-631 - Simon Friis Vindum
Spirea: A Mechanized Concurrent Separation Logic for Weak Persistent Memory. 632-657 - Sewen Thy
Adventure of a Lifetime: Extract Method Refactoring for Rust. 658-685 - Huanqi Cao
Mat2Stencil: A Modular Matrix-Based DSL for Explicit and Implicit Matrix-Free PDE Solvers on Structured Grid. 686-715 - Armaël Guéneau
Melocoton: A Program Logic for Verified Interoperability Between OCaml and C. 716-744 - André Pacak
Interactive Debugging of Datalog Programs. 745-772 - Fangke Ye
Concrete Type Inference for Code Optimization using Machine Learning with SMT Solving. 773-800 - Yu Wang
An Explanation Method for Models of Code. 801-827 - Jaehwang Jung
Modular Verification of Safe Memory Reclamation in Concurrent Separation Logic. 828-856 - Edward Lee
Simple Reference Immutability for System F. 857-881 - Zhuo Cai
Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart Contracts. 882-911 - John K. Feser
Inductive Program Synthesis Guided by Observational Program Similarity. 912-940 - Marius Müller
From Capabilities to Regions: Enabling Efficient Compilation of Lexical Effect Handlers. 941-970 - Dongjie He
A Container-Usage-Pattern-Based Context Debloating Approach for Object-Sensitive Pointer Analysis. 971-1000 - Yuandao Cai
A Cocktail Approach to Practical Call Graph Construction. 1001-1033 - Anjali Pal
Equality Saturation Theory Exploration à la Carte. 1034-1062 - Adithya Murali
Complete First-Order Reasoning for Properties of Functional Programs. 1063-1092 - Wenhao Tang
Structural Subtyping as Parametric Polymorphism. 1093-1121 - Sorawee Porncharoenwase
A Pretty Expressive Printer. 1122-1149 - Jiangyi Liu
Automated Ambiguity Detection in Layout-Sensitive Grammars. 1150-1175 - Meetesh Kalpesh Mehta
Reusing Just-in-Time Compiled Code. 1176-1197 - Arash Sahebolamri
Bring Your Own Data Structures to Datalog. 1198-1223 - Will Crichton
A Grounded Conceptual Model for Ownership Types in Rust. 1224-1252 - Quan Zhang
Building Dynamic System Call Sandbox with Partial Order Analysis. 1253-1280 - Riccardo Bianchini
Resource-Aware Soundness for Big-Step Semantics. 1281-1309 - Fengyun Liu
Initializing Global Objects: Time and Order. 1310-1337 - Anshuman Mohan
Formal Abstractions for Packet Scheduling. 1338-1362 - Ellen Arvidsson
Reference Capabilities for Flexible Memory Management. 1363-1393 - Aalok Thakkar
Mobius: Synthesizing Relational Queries with Recursive and Invented Predicates. 1394-1417 - Jin Zhou
MemPerf: Profiling Allocator-Induced Performance Slowdowns. 1418-1441 - Kirby Linvill
Verifying Indistinguishability of Privacy-Preserving Protocols. 1442-1469 - Cong Ma
Quantifying and Mitigating Cache Side Channel Leakage with Differential Set. 1470-1498 - Lisa Rennels
How Domain Experts Use an Embedded DSL. 1499-1530 - Luke Cheeseman
When Concurrency Matters: Behaviour-Oriented Concurrency. 1531-1560 - Matt D'Souza
TASTyTruffle: Just-in-Time Specialization of Parametric Polymorphism. 1561-1588 - Grant Iraci
Validating IoT Devices with Rate-Based Session Types. 1589-1617 - Thomas Haas
Static Analysis of Memory Models for SMT Encodings. 1618-1647 - Alex Renda
Turaco: Complexity-Guided Data Sampling for Training Neural Surrogates of Programs. 1648-1676 - Minki Cho
Stuttering for Free. 1677-1704 - Narges Shadab
Inference of Resource Management Specifications. 1705-1728 - Khushboo Chitre
Rapid: Region-Based Pointer Disambiguation. 1729-1757 - Max S. New
Gradual Typing for Effect Handlers. 1758-1786 - Kanghee Park
Synthesizing Specifications. 1787-1816 - Pengfei Gao
Compositional Verification of Efficient Masking Countermeasures against Side-Channel Attacks. 1817-1847 - Qiaochu Chen
Data Extraction via Semantic Regular Expression Synthesis. 1848-1877 - Orr Tamir
Counterexample Driven Quantifier Instantiations with Applications to Distributed Protocols. 1878-1904 - Shawn Meier
Historia: Refuting Callback Reachability with Message-History Logics. 1905-1934 - Jens Kanstrup Larsen
P4R-Type: A Verified API for P4 Control Plane Programs. 1935-1963 - Jacob Laurel
Synthesizing Precise Static Analyzers for Automatic Differentiation. 1964-1992 - Giovanna Kobus Conrado
Exploiting the Sparseness of Control-Flow and Call Graphs for Efficient and On-Demand Algebraic Program Analysis. 1993-2022 - Anders Miltner
Saggitarius: A DSL for Specifying Grammatical Domains. 2023-2051 - Philipp Schröer
A Deductive Verification Infrastructure for Probabilistic Programs. 2052-2082 - Chen Cui
Greedy Implicit Bounded Quantification. 2083-2111 - Yu-Fang Chen
Solving String Constraints with Lengths by Stabilization. 2112-2141 - George Zakhour
Type-Safe Dynamic Placement with First-Class Placed Values. 2142-2170 - Amirmohammad Nazari
Explainable Program Synthesis by Localizing Specifications. 2171-2195 - Angello Astorga
Perception Contracts for Safety of ML-Enabled Systems. 2196-2223 - Federico Mora
Message Chains for Distributed System Verification. 2224-2250
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 2024-11-04 20:32 CET 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 and maintained by:
the dblp computer science bibliography is funded and supported by: