PLDI 2024
2024-06-24..2024-06-28
-- online --
[PLDI 2020, PLDI 2022, PLDI 2023, PLDI 2024, PLDI 2024 Workshop Honoring Andreas Podelski, PLDI 2025, PLDI 2026, PLDI 2026 Student Research Competition]
who it's for
programming language researchers, compiler engineers, static analysis engineers, formal verification engineers, runtime engineers, performance engineers, software security researchers
topics
regex robustness checking; Bayesian-guided resource analysis; type-based points-to analysis; approximate interpretation for JS; multiversion dependency graphs; SMT theory arbitrage to bounded theories; saturation tabulation for CFL-reachability; learning visibly pushdown grammars; decidable subtyping for Julia; WebAssembly standard and performance
| title | author | length |
|---|---|---|
| Static Analysis for Checking the Disambiguation Robustness of Regular Expressions | Konstantinos Mamouras, Alexis Le Glaunec, Wu Angela Li, Agnishom Chattopadhyay | 22m |
Defines robustness as agreement between POSIX vs greedy match extraction and proves the decision problem PSPACE-complete. Builds a greedy NFA model and reduces… | ||
| Context-Free Language Reachability via Skewed Tabulation | Yuxiang Lei, Camille Bossut, Yulei Sui, Qirun Zhang | 19m |
Proposes skewed tabulation that rewrites grammars and treats certain summary edges as propagating edges so the solver avoids generating intermediary summary… | ||
| Robust Resource Bounds with Static Analysis and Bayesian Inference | Long Pham, Feras A. Saad, Jan Hoffmann | 20m |
Claims a combined static/data technique that actually implements and evaluates a hybrid: it integrates automatic amortized resource analysis (AARA) with… | ||
| Program Analysis for Adaptive Data Analysis | Jiawen Liu, Weihao Qu, Marco Gaboardi, Deepak Garg, Jonathan Ullman | 19m |
Static analysis estimates the adaptivity of while-like adaptive data analyses by building a weighted dependency graph whose node weights are reachability upper… | ||
| Scaling Type-Based Points-to Analysis with Saturation | Christian Wimmer, Codrut Stancu, David Kozak, Thomas Würthinger | 20m |
A type-based, context-insensitive points-to analysis uses a saturation threshold to stop tracking variables once their type set exceeds a limit, falling back… | ||
| Falcon: A Scalable Analytical Cache Model | Arjun Pitchanathan, Kunwar Grover, Tobias Grosser | 17m |
Falcon builds a scalable analytical model for LRU cache miss rates using polyhedral dependence analysis and by splitting analysis to avoid blowup; it evaluates… | ||
| Reducing Static Analysis Unsoundness with Approximate Interpretation | Mathias Rud Laursen, Wenyuan Xu, Anders Møller | 20m |
Introduces approximate interpretation, a dynamic phase that force-executes each function once to emit determinacy hints and feeds them into an extended… | ||
| Floating-Point TVPI Abstract Domain | Joao Rivera, Franz Franchetti, Markus Püschel | 17m |
TVPI-FP implements a two-variables-per-inequality abstract domain that allows interval coefficients to model floating-point roundoff, supports branches, loops… | ||
| Efficient Static Vulnerability Analysis for JavaScript with Multiversion Dependency Graphs | Mafalda Sofia Ferreira, Miguel Monteiro, Tiago Brito, Miguel E. Coimbra, Nuno Santos, Limin Jia, José Fragoso Santos | 20m |
Introduces Multiversion Dependency Graphs as a single, versioned object graph that records property updates and data-flow order, implemented in Graph.js and… | ||
| Interactive Abstract Interpretation with Demanded Summarization | Benno Stein, Bor-Yuh Evan Chang, Manu Sridharan | 20m |
Presents demanded summarization, an algorithm and engine that makes summary‑based abstract interpretation incremental and compositional while supporting… | ||
| SMT Theory Arbitrage: Approximating Unbounded Constraints using Bounded Theories | Benjamin Mikek, Qirun Zhang | 19m |
Transforms expensive unbounded integer and real constraints into bounded bitvector/fp versions by inferring per-constraint widths via abstract interpretation… | ||
| Inductive Approach to Spacer | Takeshi Tsukada, Hiroshi Unno | 18m |
Presents a Spacer-like CHC solver derived by structural induction that replaces global quantifier elimination with an iterative, lazy use of model-based… | ||
| SuperStack: Superoptimization of Stack-Bytecode via Greedy, Constraint-Based, and SAT(…) | Elvira Albert, Maria Garcia de la Banda, Alejandro Hernández-Cerezo, Alexey Ignatiev, Albert Rubio, Peter J. Stuckey | 18m |
SuperStack implements a stack-bytecode superoptimizer that combines a greedy bound-refinement that cuts search bounds (example reduced 13→10), a MaxSAT-based… | ||
| Hashing Modulo Context-Sensitive Alpha-Equivalence | Lasse Blaauwbroek, Miroslav Olšák, Herman Geuvers | 21m |
Defines context-sensitive alpha-equivalence as fork equivalence that coincides with bisimulation and gives a concrete hashing procedure that computes hashes… | ||
| V-Star: Learning Visibly Pushdown Grammars from Program Inputs | Xiaodong Jia, Gang Tan | 23m |
A tool called V-Star learns visibly pushdown grammars from sample inputs without prior knowledge of call/return tokens by detecting nesting patterns, inferring… | ||
| Syntactic Code Search with Sequence-to-Tree Matching: Supporting Syntactic Search with(…) | Gabriel Matute, Wode Ni, Titus Barik, Alvin Cheung, Sarah E. Chasins | 17m |
A new search architecture drops parsing and uses only tokenization plus a novel sequence-to-tree matching algorithm built on top-down tree automata to give… | ||
| PL4XGL: A Programming Language Approach to Explainable Graph Learning | Minseok Jeon, Jihyeok Park, Hakjoo Oh | 15m |
Proposes PL4XGL, a GDL-based classifier that learns models by program synthesis (top-down and bottom-up) and returns the synthesised GDL program as a provably… | ||
| Equivalence by Canonicalization for Synthesis-Backed Refactoring | Justin Lubin, Jeremy Ferguson, Kevin Ye, Jacob Yim, Sarah E. Chasins | 20m |
Presents equivalence by canonicalization: run compiler-style syntactic transforms (deforestation, partial evaluation) on both direct and combinator sketches… | ||
| (De/Re)-Composition of Data-Parallel Computations via Multi-Dimensional(…) | Ari Rasch | 18m |
Formal algebraic framework Multi-Dimensional Homomorphisms expresses data-parallel kernels with exactly three higher-order patterns (infu mdom outw), a… | ||
| A Verified Compiler for a Functional Tensor Language | Amanda Liu, Gilbert Louis Bernstein, Adam Chlipala, Jonathan Ragan-Kelley | 18m |
A mechanically verified implementation of a lowering algorithm for ATL proves that a functional tensor program lowers to imperative loop nests that write… | ||
| Stream Types | Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, Benjamin C. Pierce | 25m |
Proposes a type-theoretic foundation that lets ordinary list programs run as online stream processors by rejecting programs that need unbounded buffering and… | ||
| Numerical Fuzz: A Type System for Rounding Error Analysis | Ariel E. Kellison, Justin Hsu | 21m |
A new functional language Λnum offers a linear type system plus a novel graded monad to track local floating‑point rounding error and a sensitivity analysis to… | ||
| Decidable Subtyping of Existential Types for Julia | Julia Belyakova, Benjamin W Chung, Ross Tate, Jan Vitek | 19m |
Proves Julia’s runtime subtyping is undecidable via reduction from System F<: and designs a restricted grammar that is stratify types into method signatures… | ||
| Associated Effects: Flexible Abstractions for Effectful Programming | Matthew Lutze, Magnus Madsen | 19m |
Introduces "associated effects": type-class-level effect variables that let each instance pick its concrete effect, solving cases like total vs partial… | ||
| Space-Efficient Polymorphic Gradual Typing, Mostly Parametric | Atsushi Igarashi, Shota Ozaki, Taro Sekiyama, Yudai Tanabe | 18m |
Claim: space-efficient gradual typing becomes possible when polymorphism is restricted to mostly parametric, meaning parametricity is enforced only for… | ||
| Don’t Write, but Return: Replacing Output Parameters with Algebraic Data Types in(…) | Jaemin Hong, Sukyoung Ryu | 22m |
Automatic C-to-Rust pipeline runs a syntactic front end (czrust syntactic pass), then a static analysis based on abstract interpretation that tracks abstract… | ||
| Compiling with Abstract Interpretation | Dorian Lesbre, Matthieu Lemerre | 18m |
Turns abstract interpreters into compilers by representing domain interfaces as free algebra domains and encoding small compilation passes as domain functors… | ||
| Choral: Object-Oriented Choreographic Programming | Saverio Giallorenzo, Fabrizio Montesi, Marco Peressotti | 20m |
Choral is an object‑oriented choreographic language plus compiler that generates per-role Java libraries from choreographies expressed as classes, with a novel… | ||
| SpEQ: Translation of Sparse Codes using Equivalences | Avery Laird, Bangtian Liu, Nikolaj Bjørner, Maryam Mehri Dehnavi | 19m |
SpEQ detects implicit sparse storage, symbolically reconstructs a dense semantics, and uses an equivalence check plus lightweight runtime guards to guarantee… | ||
| Daedalus: Safer Document Parsing | Iavor S. Diatchki, Mike Dodds, Harrison Goldstein, Bill Harris, David A. Holland, Benoit Razet, Cole Schlesinger, Simon Winwood | 21m |
A domain-specific language and compiler generate safe, analyzable parsers with C++ and Haskell backends and a foreign‑function interface for things like… | ||
| Much Still to Do in Compiler Verification (A Perspective from the CakeML Project) | Magnus O. Myreen | 01h 05m |
End-to-end verified compiler for an ML-like language (the CakeML stack) compiles functions in the proof assistant logic down to concrete machine bytes and… | ||
| AI-Assisted Programming Today and Tomorrow | Nadia Polikarpova | 01h 12m |
Recent studies find GitHub Copilot has over 1M paid users and generates roughly 30–40% of active users’ code; a grounded study of 20 programmers identifies two… | ||
| The Future of Fast Code: Giving Hardware What It Wants | Jonathan Ragan-Kelley | 01h 04m |
Hardware offers huge gains but only with heavy specialization: simple Python matrix multiply hits ~10 MFLOPS, JavaScript ~500 MFLOPS, optimized C reaches ~1–40… | ||
| Wavefront Threading Enables Effective High-Level Synthesis | 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 Caulfield, Doug Burger | 21m |
Kagawa is a hardware language that maps wavefront threading directly to pipelines so the compiler does minimal work and performance is predictable; threads… | ||
| Jacdac: Service-Based Prototyping of Embedded Systems | Thomas Ball, Peli de Halleux, James Devine, Steve Hodges, Michał Moskal | 23m |
Jacdac builds a service-based stack for microcontroller prototyping that pairs each sensor or actuator with a tiny controller that advertises capabilities over… | ||
| Modular Hardware Design of Pipelined Circuits with Hazards | Minseong Jang, Jungin Rhee, Woojin Lee, Shuangshuang Zhao, Jeehoon Kang | 19m |
Proposes hazard interfaces that generalize valid-ready by carrying arbitrary “reserve” values and a ready function, plus map-reduce style combinators that… | ||
| VESTA: Power Modeling with Language Runtime Events | Joseph Raskind, Timur Babakol, Khaled Mahmoud, Yu David Liu | 20m |
VESTA builds power models from JVM runtime events (using USDT probes) and energy samples from jle/Intel RAPL, trains gradient‑boosted decision trees (XGBoost)… | ||
| Allo: A Programming Model for Composable Accelerator Design | Hongzheng Chen, Niansong Zhang, Shaojie Xiang, Zhichen Zeng, Mengjia Dai, Zhiru Zhang | 17m |
Allo is a Python-embedded ADL that decouples compute, memory, communication and data-type customizations into composable primitives and a Python-embedded ADL… | ||
| LiDO: Linearizable Byzantine Distributed Objects with Refinement-Based Liveness Proofs | Longfei Qiu, Yoonseung Kim, Ji-Yong Shin, Jieung Kim, Wolf Honore, Zhong Shao | 17m |
LiDO is a refinement-ready model that adds an explicit pacemaker state so liveness of partially synchronous Byzantine SMR reduces to a few safety invariants… | ||
| A Family of Fast and Memory Efficient Lock- and Wait-Free Reclamation | Ruslan Nikolaev, Binoy Ravindran | 21m |
Crystalline is a family of non-blocking reclamation schemes (Crystalline L, LW, W) that guarantees wait-free reclamation in its strongest variant, supports… | ||
| IsoPredict: Dynamic Predictive Analysis for Detecting Unserializable Behaviors in Weakly(…) | Chujun Geng, Spyros Blanas, Michael D. Bond, Yang Wang | 21m |
IsoPredict takes an observed serializable run, emits SMT constraints that encode weak isolation (causal/read‑committed), and searches for a feasible… | ||
| SPORE: Combining Symmetry and Partial Order Reduction | Michalis Kokologiannakis, Iason Marmanis, Viktor Vafeiadis | 20m |
SPORE is a stateless model checker that actually combines symmetry reduction and dynamic partial order reduction to cut interleavings exponentially; it proves… | ||
| A Lightweight Polyglot Code Transformation Language | Ameya Ketkar, Daniel Ramos, Lazaro Clapp, Rajkishore Barik, Murali Krishna Ramanathan | 19m |
A declarative DSL and tool called PolyglotPiranha implements composed, ordered match-replace rules that propagate context across files and languages; it runs… | ||
| CFLOBDDs: Context-Free-Language Ordered Binary Decision Diagrams | Meghana Aparna Sistla, Swarat Chaudhuri, Thomas Reps | 21m |
CFLOBDDs present a compressed Boolean-function representation that can be exponentially smaller than BDDs and, versus the decision tree, offer a… | ||
| Program Reconditioning: Avoiding Undefined Behaviour When Finding and(…) | Bastien Lecoeur, Hasan Mohsin, Alastair F. Donaldson | 19m |
Introduces reconditioning: generate potentially unsafe GPU programs, then apply a source-to-source reconditioner just before compilation so reduction never… | ||
| CQS: A Formally-Verified Framework for Fair and Abortable Synchronization | Nikita Koval, Dmitry Khalanskiy, Dan Alistarh | 15m |
CQS provides a queue-based synchronizer that implements fair FIFO ordering and efficient abortable operations by reserving array slots for suspend and resume… | ||
| Concurrent Immediate Reference Counting | Jaehwang Jung, Jeonghyeon Kim, Matthew J. Parkinson, Jeehoon Kang | 17m |
A new system, Concurrent Immediate Reference Counting, combines reference counting with SMR (EBR) to record a decrement EPO per object and use a global epoch… | ||
| Optimistic Stack Allocation and Dynamic Heapification for Managed Runtimes | Aditya Anand, Solai Adithya, Swapnil Rustagi, Priyam Seth, Vijay Sundaresan, Daryl Maier, V Krishna Nandivada, Manas Thakur | 20m |
Static + dynamic system uses a precise static escape analysis (built in Soot) to emit optimistic stack allocations into the OpenJ9 JIT, and when runtime… | ||
| Bringing the WebAssembly Standard up to Speed with SpecTec | Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas Rossberg | 16m |
SpecTec is a DSL and toolchain that serves as a single source of truth for Wasm semantics, generating typeset spec prose, formal definitions, and a meta-level… | ||
| RichWasm: Bringing Safe, Fine-Grained, Shared-Memory Interoperability Down to WebAssembly | Michael Fitzgibbons, Zoe Paraskevopoulou, Noble Mushtak, Michelle Thalakottur, Jose Sulaiman Manzur, Amal Ahmed | 21m |
RichWasm is a richly typed IR on top of WebAssembly that adds capability types, separate unrestricted (GC) and linear (unique-owner) memories, and… | ||
| Linear Matching of JavaScript Regular Expressions | Aurèle Barrière, Clément Pit-Claudel | 23m |
Presents a proof that a much larger subset of JavaScript regexes admits linear-time matching, identifies semantic bugs and superlinear cases in V8’s linear… | ||
| Boosting Compiler Testing by Injecting Real-World Code | Shaohua Li, Theodoros Theodoridis, Zhendong Su | 22m |
Tool Creal injects real-world functions into Csmith-generated seeds, extracting 50,000 functions from 100+ popular GitHub projects, inferring input/output… | ||
| Diffy: Data-Driven Bug Finding for Configurations | Siva Kesava Reddy Kakarla, Francis Y. Yan, Ryan Beckett | 22m |
Diffy automatically synthesizes structured configuration templates with holes, then flags anomalous template parameters using unsupervised anomaly detection… | ||
| Compatible Branch Coverage Driven Symbolic Execution for Efficient Bug Finding | Qiuping Yi, Yifan Yu, Guowei Yang | 14m |
Implements a static dependence analysis to compute a Compatible Branch Set that lets symbolic execution soundly prune branches that do not add new branch… | ||
| Refined Input, Degraded Output: The Counterintuitive World of Compiler Behavior | Theodoros Theodoridis, Zhendong Su | 20m |
Automated pipeline instruments C programs generated by cith with runtime checks, then injects compiler builtins (unreachable/assume) to encode observed dead… | ||
| Hyperblock Scheduling for Verified High-Level Synthesis | Yann Herklotz, John Wickerson | 22m |
A verified HLS backend implements a hyperblock scheduler with operation chaining and a system-of-difference-constraints LP scheduler, emits schedules checked… | ||
| RefinedRust: A Type System for High-Assurance Verification of Rust Programs | Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer | 17m |
RefinedRust presents a refinement type system that verifies both unsafe Rust and safe Rust by translating MIR into a Coq-embedded Rust model and checking… | ||
| Verified Extraction from Coq to OCaml | Yannick Forster, Matthieu Sozeau, Nicolas Tabareau | 21m |
A verified extraction pipeline implemented in Coq proves that programs over first‑order inductive data types extracted from Coq safely interoperate with OCaml… | ||
| Towards Trustworthy Automated Program Verifiers: Formally Validating Translations into(…) | Gaurav Parthasarathy, Thibault Dardinier, Benjamin Bonneau, Peter Müller, Alexander J. Summers | 18m |
Adds a per-run Isabelle certificate generator to an existing Viper→Boogie translation, proving that whenever the generated Boogie program has no failing… | ||
| An Algebraic Language for Specifying Quantum Networks | Anita Buckley, Pavel Chuprikov, Rodrigo Otoni, Robert Soulé, Robert Rand, Patrick Eugster | 17m |
Defines BellKAT — a Kleene-algebra based language whose semantics live in a new algebra BellSKA and whose basic primitives are… | ||
| Compiling Conditional Quantum Gates without Using Helper Qubits | Keli Huang, Jens Palsberg | 17m |
Compiles an n‑qubit conditional into a linear number of two‑qubit conditionals without helper qubits, using 278n gates overall and empirically requiring 1/3 as… | ||
| The T-Complexity Costs of Error Correction for Control Flow in Quantum Computation | Charles Yuan, Michael Carbin | 19m |
Identifies that common control-flow constructs cause polynomial increases in T-complexity under surface-code error correction and gives a precise cost model… | ||
| Qubit Recycling Revisited | Hanru Jiang | 19m |
Reframes qubit recycling as a graph-plus-matrix problem: introduce Qubit Dependency Graphs and show recycling reduces to an independent row/column permutation… | ||
| Compilation of Qubit Circuits to Optimized Qutrit Circuits | Ritvik Sharma, Sara Achour | 20m |
An optimizing compiler called Dare converts qubit circuits into qutrit circuits by a novel qutrit decomposition plus a rewrite engine that applies both… | ||
| Automated Verification of Fundamental Algebraic Laws | George Zakhour, Pascal Weisenburger, Guido Salvaneschi | 19m |
A verifier called Propel automatically conjectures and proves auxiliary lemmas (distributivity, generalizations) for a purely functional Scala subset, uses… | ||
| Input-Relational Verification of Deep Neural Networks | Debangshu Banerjee, Changming Xu, Gagandeep Singh | 17m |
A verifier that reasons about multiple executions builds a DiffPoly abstract domain to track concrete and symbolic difference bounds layer by layer, produces… | ||
| A Proof Recipe for Linearizability in Relaxed Memory Separation Logic | Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang | 19m |
This work gives a concrete proof recipe and mechanization in Coq (Iris-based iRC11) that reduces manual effort by about 81% via automation, introduces object… | ||
| Reward-Guided Synthesis of Intelligent Agents with Control Structures | Guofeng Cui, Yuning Wang, Wenjie Qiu, He Zhu | 24m |
ReGuS directly synthesizes readable control programs from sparse reward signals using a hierarchical algorithm that decomposes loop search, performs on-demand… | ||
| Recursive Program Synthesis using Paramorphisms | Qiantan Hong, Alex Aiken | 25m |
Claims a synthesis method that fixes recursive shape with multi-hole templates and fills holes by stochastic search for nonrecursive straight-line code, using… | ||
| Superfusion: Eliminating Intermediate Data Structures via Inductive Synthesis | Ruyi Ji, Yuwei Zhao, Nadia Polikarpova, Yingfei Xiong, Zhenjiang Hu | 40m |
Superfusion uses inductive program synthesis to remove intermediate collections by synthesizing a small compression function that maps packed structures to… | ||
| From Batch to Stream: Automatic Generation of Online Algorithms | Ziteng Wang, Shankara Pailoor, Aaryan Prakash, Yuepeng Wang, Işıl Dillig | 23m |
Automated method extracts a relational function signature via static analysis, builds initial state by evaluating each spec on the empty list, and synthesizes… | ||
| A HAT Trick: Automatically Verifying Representation Invariants using Symbolic Finite(…) | Zhe Zhou, Qianchuan Ye, Benjamin Delaware, Suresh Jagannathan | 17m |
Describes a toolchain that uses symbolic finite automata to encode data-dependent, temporal representation invariants and integrates them into a refinement… | ||
| Hyper Hoare Logic: (Dis-)Proving Program Hyperproperties | Thibault Dardinier, Peter Müller | 20m |
Logic lifts pre/postconditions to properties of arbitrary sets of states and claims to capture exactly the class of hyperproperties over terminating… | ||
| Mechanised Hypersafety Proofs about Structured Data | Vladimir Gladshtein, Qiyuan Zhao, Willow Ahrens, Saman Amarasinghe, Ilya Sergey | 21m |
Claims a practical verification path: LGTM encodes formats as getter code and proves correctness via parametrised hypersafety triples mechanised as a Coq… | ||
| Predictable Verification using Intrinsic Definitions | Adithya Murali, Cody Rivera, P. Madhusudan | 19m |
Proposes that defining heap structures with intrinsic definitions — auxiliary monadic maps plus local constraints — makes verification decidable and therefore… | ||
| Live Verification in an Interactive Proof Assistant | Samuel Gruetter, Viktor Fukala, Adam Chlipala | 21m |
Prototype implements live verification after each line inside Coq, parsing polyglot C/Coq files and updating a concise symbolic state view while editing; it… | ||
| Maximum Consensus Floating Point Solutions for Infeasible Low-Dimensional Linear(…) | Mridul Aanjaneya, Santosh Nagarakatte | 18m |
Claims an algorithm that finds a maximum consensus floating point solution for infeasible low-dimensional linear programs with billions of constraints and few… | ||
| Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq | Simon Spies, Lennard Gäher, Michael Sammler, Derek Dreyer | 20m |
Quiver claims automated inference of full separation logic specs for C code while verifying soundness in Coq using Iris, implemented as a prototype atop… | ||
| The Functional Essence of Imperative Binary Search Trees | Anton Lorenzen, Daan Leijen, Wouter Swierstra, Sam Lindley | 20m |
Functional algorithms introduce a new first-class constructor context primitive and use Koka’s reuse-aware reference counting to implement tail-call, in-place… | ||
| Foundational Integration Verification of a Cryptographic Server | Andres Erbsen, Jade Philipoom, Dustin Jamner, Ashley Lin, Samuel Gruetter, Clément Pit-Claudel, Adam Chlipala | 20m |
A verified bare-metal garage-door server implements authenticated open/close commands and prevents replays by rotating seeds, and a single machine-checked… | ||
| Quest Complete: The Holy Grail of Gradual Security | Tianyu Chen, Jeremy G. Siek | 22m |
Claims a language 𝜆★IFC that satisfies both noninterference and the gradual guarantee by removing the unknown label ★ from runtime security labels, keeping… | ||
| Quantitative Robustness for Vulnerability Assessment | Guillaume Girol, Guilhem Lacombe, Sébastien Bardin | 16m |
Defines quantitative robustness as the maximum proportion of uncontrolled inputs that hit a target location for some fixed controlled input and implements… | ||
| A Tensor Compiler with Automatic Data Packing for Simple and Efficient Fully Homomorphic(…) | Aleksandar Krastev, Nikola Samardzic, Simon Langowski, Srinivas Devadas, Daniel Sanchez | 20m |
Fhelipe is a tensor-to-FHE compiler that implements automatic data packing and a layout algebra (bit-permutation + gap bits) to pack tensors into CKKS… | ||
| KATch: A Fast Symbolic Verifier for NetKAT | Mark Moeller, Jules Jacobs, Olivier Savary Belanger, David Darais, Cole Schlesinger, Steffen Smolka, Nate Foster, Alexandra Silva | 17m |
KATch implements NetKAT verification in Scala and replaces exhaustive packet enumeration with symbolic packets, BDD-style relations called SPs that are… | ||
| NetBlocks: Staging Layouts for High-Performance Custom Host Network Stacks | Ajay Brahmakshatriya, Chris Rinard, Manya Ghobadi, Saman Amarasinghe | 24m |
NetBlocks is a DSL plus compiler that stages protocol features and packet layouts to generate specialized host network stacks using the BuildIt staging… | ||
| Consolidating Smart Contracts with Behavioral Contracts | Guannan Wei, Danning Xie, Wuqi Zhang, Yongwei Yuan, Zhuo Zhang | 19m |
ConSol extends Solidity with a transpiler that attaches behavioral contracts to first-class addresses by expanding 160-bit addresses into a guarded address… | ||
| Static Posterior Inference of Bayesian Probabilistic Programming via Polynomial Solving | Peixin Wang, Tengshun Yang, Hongfei Fu, Guanyan Li, C.-H. Luke Ong | 20m |
Derives guaranteed upper and lower bounds for normalized posteriors by reducing inference to polynomial solving over templates guided by a new fixed‑point… | ||
| Probabilistic Programming with Programmable Variational Inference | McCoy R. Becker, Alexander K. Lew, Xiaoyan Wang, Matin Ghavami, Mathieu Huot, Martin C. Rinard, Vikash K. Mansinghka | 21m |
Proposes a compositional, provably correct route to variational inference that turns user-written model, guide, and objective programs into unbiased gradient… | ||
| GenSQL: A Probabilistic Programming System for Querying Generative Models of Database(…) | Mathieu Huot, Matin Ghavami, Alexander K. Lew, Ulrich Schaechtle, Cameron E. Freer, Zane Shelby, Martin C. Rinard, Feras A. Saad, Vikash K. Mansinghka | 20m |
GenSQL is a SQL extension that runs Bayesian queries over generative table models, provides a unified model API (supports PPLs, GLMs, CTGAN, and a… | ||
| Equivalence and Similarity Refutation for Probabilistic Programs | Krishnendu Chatterjee, Ehsan Kafshdar Goharshady, Petr Novotný, Đorđe Žikelić | 18m |
Searches for a concrete output function f and automated certificates—an upper expectation supermartingale for one program and a lower expectation submartingale… | ||
| Compiling Probabilistic Programs for Variable Elimination with Information Flow | Jianlin Li, Eric Wang, Yizhou Zhang | 19m |
This paper presents a compiler, Maple, that uses an information-flow type system to partition and eliminate discrete latent variables in recursive… | ||
| Bit Blasting Probabilistic Programs | Poorva Garg, Steven Holtzen, Guy Van den Broeck, Todd Millstein | 20m |
Presents a new discretization called bit blasting that encodes continuous variables as Boolean bits so a domain of 2^b points becomes a discrete program over… | ||
| nothing matches | ||