OOPSLA2 2026 – Author Index |
Contents -
Abstracts -
Authors
|
A B C D E F G H I J K L M N O P Q R S T V W X Y Z
| Aamer, Zain K. |
Zain K. Aamer and Benjamin C. Pierce (University of Pennsylvania, USA) |
|
| Abramsky, Samson |
Samson Abramsky and Radha Jagadeesan (University College London, UK; DePaul University, USA) Existing quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with named reversible operations provide domain-level control spaces without exposing tag management. Every well-typed term—including at function type—denotes a unitary on its boundary interface, and the compiler realizes exactly its wiring as a quantum circuit on the physical qubit layout (assuming correctness of the pytket backend). Granthi is implemented end-to-end: an OCaml DSL elaborates surface programs through a binder-free core IR to executable quantum circuits via pytket. The language directly supports the quantum switch—the paper’s running example, compiled to a static circuit—as well as interference on control-flow history and structured finite control, all within the purely unitary fragment. |
|
| Adams, Michael D. |
Luyu Cheng, Florent Ferrari, Lionel Parreaux, and Michael D. Adams (Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France; National University of Singapore, Singapore) |
|
| Agarwal, Sudhanshu |
Sudhanshu Agarwal and Saugata Ghose (University of Illinois at Urbana-Champaign, USA) |
|
| Ahn, Sehyuk |
Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu (KAIST, Republic of Korea) Programming languages evolve over time, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, like JavaScript and WebAssembly (Wasm), keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and Wasm specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. Both framework designs leverage the existence of JavaScript and Wasm’s normative specifications, which is not the case for many languages. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 is a statically-typed domain-specific language for programming packet processors. It is evolving without a normative specification, thereby introducing inconsistencies and errors into the P4 ecosystem. From a mechanization framework perspective, P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain. We share the lessons learned from our case study, to provide insights for integrating mechanization into real-world languages without normative specifications. |
|
| Aiken, Alex |
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India; Google DeepMind, India) Elliott Slaughter, Rupanshu Soi, Michael Bauer, and Alex Aiken (SLAC National Accelerator Laboratory, USA; Stanford University, USA; NVIDIA Research, USA) Checkpointing, or periodic saving of program state to storage, is the de facto standard technique used to mitigate risks of nondeterministic bugs, hardware faults, and job wall-time limits in long-running programs. Traditional approaches require users to manually manage the migration of data to and from storage when capturing checkpoints and when resuming execution. However, for task-based programs, where the user has already factored the computation into tasks and the program data into collections, sufficient information is available to automatically capture and resume from checkpoints with minimal code changes. We present Relight, the first framework for automatic, distributed checkpointing of task-based programs that provides an efficient fast-forward replay for full job recovery. On a set of already-optimized benchmarks, we demonstrate that Relight delivers checkpointing performance and scalability comparable to the original, unmodified codes when running on up to 512 nodes of the Piz Daint supercomputer. |
|
| Antoch, Jaromír |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Aotani, Tomoyuki |
Tomoyuki Aotani and Tetsuo Kamina (Sanyo-Onoda City University, Japan; Oita University, Japan) |
|
| Arlt, Ellen |
Hongyi Ling, Thibault Dardinier, Ellen Arlt, and Peter Müller (ETH Zurich, Switzerland; EPFL, Switzerland; MPI-SWS, Germany) Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL. Ellen Arlt and Viktor Vafeiadis (MPI-SWS, Germany) |
|
| Arora, Jai |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Askarov, Aslan |
Magnus Madsen, Andreas Stenbæk Larsen, Jakob Schneider Villumsen, and Aslan Askarov (Aarhus University, Denmark) Today, most software is developed by building on packages, allowing developers to accelerate development. The proliferation of package dependencies creates a target-rich environment for malicious actors to hijack packages to inject malware, steal sensitive information, or cause destruction. Such supply chain attacks constantly threaten package ecosystems such as Cargo, npm, and Maven. In this paper, we explore how to fight against such attacks by leveraging effect systems. While effect systems predict the behavior of software components, there is a practical gap between a programming language with an effect system and a programming language ecosystem that can use such effects to thwart attacks. To close this gap, we introduce a notion of an effect-safe package upgrade and develop an effect-aware package manager that enforces safety through effect lock files. We extend the Flix programming language and its compiler toolchain with an effect-aware package manager. We evaluate the usefulness of the proposed effect-aware package manager with a case study of 51 supply chain attacks from the "Backstabbers Knife Collection" corpus of malware. The study suggests that 48 of these attacks are likely preventable with our proposed effect-aware package manager. |
|
| Bai, Alexander Y. |
Dinghong Zhong, Alexander Y. Bai, Mikail Khan, and Guannan Wei (Tufts University, USA; New York University, USA; Carnegie Mellon University, USA) |
|
| Bai, Yudi |
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl (University of Waterloo, Canada) |
|
| Bandukwala, Alexander |
Alexander Bandukwala and Cyrus Omar (University of Michigan, USA) |
|
| Bao, Yuyan |
Yuyan Bao and Tiark Rompf (Augusta University, USA; Purdue University, USA) |
|
| Baradaran, Sara |
Sara Baradaran, Yifei Huang, Wei Le, and Mukund Raghothaman (University of Southern California, USA; Iowa State University, USA) |
|
| Basin, David |
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin (ETH Zurich, Switzerland) Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems. The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination. We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds. |
|
| Batz, Kevin |
Katherine Wu, Jules Jacobs, Kevin Batz, and Alexandra Silva (Cornell University, USA; Jane Street, USA) |
|
| Bauer, Michael |
Elliott Slaughter, Rupanshu Soi, Michael Bauer, and Alex Aiken (SLAC National Accelerator Laboratory, USA; Stanford University, USA; NVIDIA Research, USA) Checkpointing, or periodic saving of program state to storage, is the de facto standard technique used to mitigate risks of nondeterministic bugs, hardware faults, and job wall-time limits in long-running programs. Traditional approaches require users to manually manage the migration of data to and from storage when capturing checkpoints and when resuming execution. However, for task-based programs, where the user has already factored the computation into tasks and the program data into collections, sufficient information is available to automatically capture and resume from checkpoints with minimal code changes. We present Relight, the first framework for automatic, distributed checkpointing of task-based programs that provides an efficient fast-forward replay for full job recovery. On a set of already-optimized benchmarks, we demonstrate that Relight delivers checkpointing performance and scalability comparable to the original, unmodified codes when running on up to 512 nodes of the Piz Daint supercomputer. |
|
| Bellante, Armando |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Berlstein, Griffin |
Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, and Adrian Sampson (Cornell University, USA) |
|
| Besson, Frédéric |
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen (Zhejiang University, China; Inria Rennes, France; Inria, France) |
|
| Bhat, Siddharth |
Siddharth Bhat, Léo Stefanesco, George Rennie, John Regehr, and Tobias Grosser (University of Cambridge, UK; University of Utah, USA) |
|
| Bieniusa, Annette |
Julian Haas, Ragnar Mogk, Annette Bieniusa, and Mira Mezini (Technische Universität Darmstadt, Germany; Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Germany) |
|
| Binder, Walter |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. Júnior Löff, Daniele Bonetta, and Walter Binder (USI Lugano, Switzerland; VU Amsterdam, Netherlands) Strings are the primary mechanism through which Java applications ingest external textual data, including data read from files, databases, network interfaces, and native libraries. In data-intensive applications, such data must either be materialized as heap-allocated java.lang.String objects, incurring allocation, copying, encoding, and garbage-collection costs, or accessed through low-level and unsafe foreign-memory mechanisms that require non-standard string APIs and explicit reasoning about memory management and object lifetimes. Neither option is well suited to high-volume ingestion workloads that require both efficiency and seamless integration with existing Java code. We present TwinString, an alternative representation of java.lang.String that decouples string semantics from the physical placement of its contents. A TwinString stores its data outside the regular Java heap while preserving the standard String type and behavior expected by Java programs and libraries. VM support controls this data and manages its lifetime with garbage collection, allowing foreign textual data to be exposed as ordinary strings without introducing additional custom string types. We implement TwinStrings in GraalVM Native Image and evaluate them across several workloads, including microbenchmarks, text-processing applications over real-world datasets, and data-heavy applications using JDBC and SQLite. The results show that TwinStrings significantly reduce allocation overhead while remaining compatible with the original String API, and reduce P99.9 tail latency by up to 42.2% in realistic library and JDBC workloads by alleviating heap allocation and garbage-collection pressure. |
|
| Blackshear, Sam |
Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey (Mysten Labs, USA; Stanford University, USA; Microsoft, USA; National University of Singapore, Singapore) Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date. |
|
| Blanas, Spyros |
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, and Yang Wang (Ohio State University, USA) Relational data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation for scalable performance, permitting sporadic unserializable executions that produce incorrect results or failures. Prior work uses dynamic predictive analysis to infer violations from execution traces, but existing techniques cannot handle relational (i.e., SQL) queries with complex predicates, and they predict executions that do not violate View Serializability, leading to false negatives and false positives. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in OLTP-Bench programs and in the widely used e-commerce application Spree. |
|
| Böck, Markus |
Markus Böck and Jürgen Cito (TU Wien, Austria) Universal probabilistic programming languages (PPLs) enable the specification of models with stochastic support structure. Posterior inference is notoriously hard for this class of models and remains difficult to accelerate on modern hardware. In response to these challenges, we introduce Upix - the first probabilistic programming system that realises the divide-conquer-combine (DCC) inference algorithm as a framework. In Upix, a model expressed in a universal PPL is automatically split into multiple sub-models with static support structure, which are then compiled with JAX for execution on accelerator hardware. The system allows extensive customisation of inference algorithms by incorporating established concepts from programmable inference literature. To evaluate our system, we implemented two existing DCC algorithms in Upix and instantiated three novel algorithms. We show that our implementation can result in better approximation quality compared to existing approaches by achieving up to 1070 times more computation within the same time budget. On machines with up to 64 CPU cores and 8 GPU devices, we demonstrate that Upix enables the scaling of inference algorithms to workloads that are impractically slow for CPUs and prior methods. |
|
| Boďa, Tomáš |
Tomas Petricek and Tomáš Boďa (Charles University, Czech Republic) |
|
| Bommineni, Chathur |
Benjamin Mikek, Chathur Bommineni, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) |
|
| Bond, Michael D. |
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, and Yang Wang (Ohio State University, USA) Relational data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation for scalable performance, permitting sporadic unserializable executions that produce incorrect results or failures. Prior work uses dynamic predictive analysis to infer violations from execution traces, but existing techniques cannot handle relational (i.e., SQL) queries with complex predicates, and they predict executions that do not violate View Serializability, leading to false negatives and false positives. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in OLTP-Bench programs and in the widely used e-commerce application Spree. |
|
| Bonetta, Daniele |
Júnior Löff, Daniele Bonetta, and Walter Binder (USI Lugano, Switzerland; VU Amsterdam, Netherlands) Strings are the primary mechanism through which Java applications ingest external textual data, including data read from files, databases, network interfaces, and native libraries. In data-intensive applications, such data must either be materialized as heap-allocated java.lang.String objects, incurring allocation, copying, encoding, and garbage-collection costs, or accessed through low-level and unsafe foreign-memory mechanisms that require non-standard string APIs and explicit reasoning about memory management and object lifetimes. Neither option is well suited to high-volume ingestion workloads that require both efficiency and seamless integration with existing Java code. We present TwinString, an alternative representation of java.lang.String that decouples string semantics from the physical placement of its contents. A TwinString stores its data outside the regular Java heap while preserving the standard String type and behavior expected by Java programs and libraries. VM support controls this data and manages its lifetime with garbage collection, allowing foreign textual data to be exposed as ordinary strings without introducing additional custom string types. We implement TwinStrings in GraalVM Native Image and evaluate them across several workloads, including microbenchmarks, text-processing applications over real-world datasets, and data-heavy applications using JDBC and SQLite. The results show that TwinStrings significantly reduce allocation overhead while remaining compatible with the original String API, and reduce P99.9 tail latency by up to 42.2% in realistic library and JDBC workloads by alleviating heap allocation and garbage-collection pressure. |
|
| Bourgeat, Thomas |
Guokai Chen, Sergi Soler Arrufat, Clément Pit-Claudel, and Thomas Bourgeat (EPFL, Switzerland) |
|
| Bovel, Matt |
Matt Bovel, Viktor Kunčak, and Martin Odersky (EPFL, Switzerland) |
|
| Bračevac, Oliver |
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky (EPFL, Switzerland) Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument” become inexpressible. Both arise in the Scala 3 standard library: Try re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and Future must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion (c.only[C]) and exclusion (c.except[C]). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns. |
|
| Bruni, Roberto |
Roberto Bruni, Lorenzo Gazzella, and Roberta Gori (University of Pisa, Italy) |
|
| Bulej, Lubomír |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Caldwell, Ben |
Ben Caldwell, William Spencer, Aleks Kissinger, and Robert Rand (University of Chicago, USA; University of Oxford, UK) Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition obscures the essential connective information, leading to longer proofs filled with syntactic manipulation. To address the gap between proof assistants and paper proofs, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning over these systems. Our tactics can also be used in existing verification projects about symmetric monoidal categories that can be treated as tensors. |
|
| Cao, David Minh-Duy |
Parker Ziegler, David Minh-Duy Cao, Justin Lubin, and Sarah E. Chasins (University of California at Berkeley, USA) |
|
| Cao, Tianci |
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen (Zhejiang University, China; Inria Rennes, France; Inria, France) |
|
| Cea Fernández, María |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Chabbi, Milind |
Elton Pinto and Milind Chabbi (Georgia Institute of Technology, USA; Uber Technologies, USA) |
|
| Charlton, Noah |
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, and Yang Wang (Ohio State University, USA) Relational data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation for scalable performance, permitting sporadic unserializable executions that produce incorrect results or failures. Prior work uses dynamic predictive analysis to infer violations from execution traces, but existing techniques cannot handle relational (i.e., SQL) queries with complex predicates, and they predict executions that do not violate View Serializability, leading to false negatives and false positives. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in OLTP-Bench programs and in the widely used e-commerce application Spree. |
|
| Chasins, Sarah E. |
Parker Ziegler, David Minh-Duy Cao, Justin Lubin, and Sarah E. Chasins (University of California at Berkeley, USA) |
|
| Chen, Guokai |
Guokai Chen, Sergi Soler Arrufat, Clément Pit-Claudel, and Thomas Bourgeat (EPFL, Switzerland) |
|
| Chen, Hongyu |
Hongyu Chen, Yu Wang, Jianhua Zhao, and Ke Wang (Nanjing University, China) Compiler backends are critical for translating high-level code into efficient machine instructions, yet they remain relatively underexplored in compiler testing. Effective backend testing requires programs that expose low-level backend behaviors, but such features are difficult to generate and are frequently eliminated by earlier optimization passes. As a result, existing testing approaches often fail to adequately exercise backend behaviors and are therefore less effective at uncovering backend defects. We present BackSmith, a black-box approach for testing compiler backends across compilers and architectures. BackSmith generates code snippets with two complementary properties: backend-oriented features that directly stress backend mechanisms such as instruction selection and register allocation, and optimization-resistant features that preserve program diversity by resisting excessive middle-end canonicalization. To further increase coverage of rare but critical backend behaviors, BackSmith also generates code snippets whose compiled assembly rarely arises during random generation. It then integrates all three kinds of features into seed programs for backend testing. We evaluated BackSmith on 16 mature GCC and LLVM backends. Over five months of testing, BackSmith uncovered 104 previously unknown backend bugs, 88 of which have been confirmed or fixed, demonstrating the effectiveness of our approach in systematically exposing backend defects. |
|
| Chen, Jiawei |
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin (University of Michigan, USA; Shanghai University of Finance and Economics, China) Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art. |
|
| Chen, Mingshuai |
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen (Zhejiang University, China; Inria Rennes, France; Inria, France) |
|
| Chen, Qinlin |
Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. |
|
| Chen, Wei |
Sixiang Peng, Chenyang Sun, Wei Chen, Bowen Zhang, and Charles Zhang (Hong Kong University of Science and Technology, China) The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries. |
|
| Chen, Xingchu |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Chen, Yu-Fang |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| Chen, Yusen |
Peishan Huang, Wenmeng Zhang, Yusen Chen, and Zhenbang Chen (National University of Defense Technology, China) |
|
| Chen, Zhenbang |
Yide Du, Zhenbang Chen, Weijiang Hong, and Wei Dong (National University of Defense Technology, China) Peishan Huang, Wenmeng Zhang, Yusen Chen, and Zhenbang Chen (National University of Defense Technology, China) |
|
| Cheng, Luyu |
Luyu Cheng, Florent Ferrari, Lionel Parreaux, and Michael D. Adams (Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France; National University of Singapore, Singapore) |
|
| Ching, Jeffrey |
Jeffrey Ching and Danfeng Zhang (Duke University, USA) |
|
| Cho, Kyeongmin |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. |
|
| Choi, Jaeho |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. |
|
| Chow, Sherman S. M. |
Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, and Guoqiang Li (Shanghai Jiao Tong University, China; Chinese University of Hong Kong, Hong Kong; Shanghai University of Finance and Economics, China; Sun Yat-sen University, China) |
|
| Cirac, J. Ignacio |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Cito, Jürgen |
Markus Böck and Jürgen Cito (TU Wien, Austria) Universal probabilistic programming languages (PPLs) enable the specification of models with stochastic support structure. Posterior inference is notoriously hard for this class of models and remains difficult to accelerate on modern hardware. In response to these challenges, we introduce Upix - the first probabilistic programming system that realises the divide-conquer-combine (DCC) inference algorithm as a framework. In Upix, a model expressed in a universal PPL is automatically split into multiple sub-models with static support structure, which are then compiled with JAX for execution on accelerator hardware. The system allows extensive customisation of inference algorithms by incorporating established concepts from programmable inference literature. To evaluate our system, we implemented two existing DCC algorithms in Upix and instantiated three novel algorithms. We show that our implementation can result in better approximation quality compared to existing approaches by achieving up to 1070 times more computation within the same time budget. On machines with up to 64 CPU cores and 8 GPU devices, we demonstrate that Upix enables the scaling of inference algorithms to workloads that are impractically slow for CPUs and prior methods. |
|
| Crichton, Will |
Gavin Gray, Shriram Krishnamurthi, and Will Crichton (Brown University, USA) |
|
| Crupi, Marianna |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Cui, Jiacai |
Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. |
|
| Dai, Yihan |
Yihan Dai, Sijie Liang, Haotian Xu, Peichu Xie, and Sergey Mechtaev (Peking University, China; Beijing Forestry University, China; Independent, China) |
|
| Daiyou, Wu |
Xinchen Yao, Wu Daiyou, and Zhiqiang Zuo (Nanjing University, China) Capturing the control-flow and/or coverage profiles of Python code becomes a pressing need for Python development community, which is commonly used in a wide spectrum of tasks including program testing/fuzzing, debugging, understanding, and optimizations. Existing tracing approaches either suffer from prohibitively high overhead or only collect approximate information, which cannot satisfy the practical requirements. In this paper, we propose to leverage modern hardware tracing modules to achieve precise and low-overhead control-flow tracing for Python programs. To this goal, we develop Pyriscope on top of CPython runtime by integrating the effective trace pruning and efficient analysis techniques. Evaluation results demonstrate the efficacy of our system. It incurs an average overhead of only 2.99% for rich-informative control-flow tracing, which is orders of magnitude smaller than that of the state of the arts. |
|
| D'Antoni, Loris |
Jinwoo Kim, Victor Nicolet, Joey Dodds, and Loris D'Antoni (University of California at San Diego, USA; Amazon, USA) |
|
| Dardinier, Thibault |
Hongyi Ling, Thibault Dardinier, Ellen Arlt, and Peter Müller (ETH Zurich, Switzerland; EPFL, Switzerland; MPI-SWS, Germany) Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL. |
|
| Devarakonda, Vasudha |
Dat Nguyen, Vasudha Devarakonda, Anxiao Jiang, and Khanh Nguyen (Texas A&M University, USA) |
|
| Di, Nongyu |
Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma (Nanjing University, China; ETH Zurich, Switzerland) As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either. |
|
| Dietl, Werner |
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl (University of Waterloo, Canada) |
|
| Dillig, Işıl |
Anders Møller and Işıl Dillig (Aarhus University, Denmark; University of Texas at Austin, USA) |
|
| Ding, Ling |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Dodds, Joey |
Jinwoo Kim, Victor Nicolet, Joey Dodds, and Loris D'Antoni (University of California at San Diego, USA; Amazon, USA) |
|
| Donat-Bouillud, Pierre |
Mickaël Laurent, Pierre Donat-Bouillud, Filip Křikava, and Jan Vitek (Charles University, Czech Republic; Czech Technical University, Czech Republic) Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple---a row variable maps to a single row---and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch. |
|
| Dong, Rongcui |
Jingyu Qiu, Rongcui Dong, and Sreepathi Pai (University of Rochester, USA) |
|
| Dong, Wei |
Yide Du, Zhenbang Chen, Weijiang Hong, and Wei Dong (National University of Defense Technology, China) |
|
| Dreyer, Derek |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Driscoll, Benjamin |
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India; Google DeepMind, India) |
|
| Du, Yide |
Yide Du, Zhenbang Chen, Weijiang Hong, and Wei Dong (National University of Defense Technology, China) |
|
| Dubey, Kshitij |
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India; Google DeepMind, India) |
|
| Dyce, Evan |
Xiaoyu Liu, Qikang Liu, Evan Dyce, Keval Vora, and Yuepeng Wang (Simon Fraser University, Canada) Writing graph queries is challenging for non-experts due to the complexity of graph data models and the need to identify proper graph patterns. While recent research has advanced query synthesis for relational and document databases, the problem of synthesizing graph queries remains under-explored. We present a novel approach for synthesizing graph queries from computation demonstrations, where users specify the desired output through expressions over properties of input graphs. Our method addresses the challenge of inferring meaningful graph patterns for matching and efficiently constructing the remaining components of the query. Specifically, we combine graph mining, which identifies candidate patterns across input graphs, with deduction-based pruning, which guides an efficient synthesis of the filtering predicate and return clause. We have implemented our approach in a tool called DMiner and evaluated it on 90 benchmarks. Experimental results show that DMiner successfully synthesizes desired queries for 87 benchmarks, with an average synthesis time of 0.6 seconds per query. This outperforms both enumerative search and LLM baselines. We also conducted a user study, which shows that users can provide demonstrations with modest effort and 87.5% of the provided demonstrations are sufficient for DMiner to synthesize the desired query. |
|
| Elazar Mittelman, Segev |
Segev Elazar Mittelman, Harrison Goldstein, and Leonidas Lampropoulos (University of Maryland, College Park, USA; University at Buffalo, USA) |
|
| Fan, Andong |
Andong Fan, Lionel Parreaux, and Ningning Xie (University of Toronto, Canada; Hong Kong University of Science and Technology, Hong Kong) |
|
| Farquet, François |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Ferrari, Florent |
Luyu Cheng, Florent Ferrari, Lionel Parreaux, and Michael D. Adams (Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France; National University of Singapore, Singapore) |
|
| Fischer, Roman |
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin (ETH Zurich, Switzerland) Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems. The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination. We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds. |
|
| Fischman, Alex |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Flatt, Oliver |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Florido-Llinàs, Marta |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Frigo, Marco |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Fu, Hongfei |
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin (University of Michigan, USA; Shanghai University of Finance and Economics, China) Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art. Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, and Guoqiang Li (Shanghai Jiao Tong University, China; Chinese University of Hong Kong, Hong Kong; Shanghai University of Finance and Economics, China; Sun Yat-sen University, China) |
|
| Gäher, Lennard |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Galán Pascual, Daniel |
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin (ETH Zurich, Switzerland) Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems. The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination. We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds. |
|
| Gazzella, Lorenzo |
Roberto Bruni, Lorenzo Gazzella, and Roberta Gori (University of Pisa, Italy) |
|
| Geng, Chujun |
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, and Yang Wang (Ohio State University, USA) Relational data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation for scalable performance, permitting sporadic unserializable executions that produce incorrect results or failures. Prior work uses dynamic predictive analysis to infer violations from execution traces, but existing techniques cannot handle relational (i.e., SQL) queries with complex predicates, and they predict executions that do not violate View Serializability, leading to false negatives and false positives. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in OLTP-Bench programs and in the widely used e-commerce application Spree. |
|
| Ghose, Saugata |
Sudhanshu Agarwal and Saugata Ghose (University of Illinois at Urbana-Champaign, USA) |
|
| Gladshtein, Vladimir |
Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey (National University of Singapore, Singapore; Princeton University, USA) Relational program logics are a popular formalism for stating and proving properties that relate executions of several computations. We present Infinitary Relational Logic (IRL)—the first Hoare-style Separation Logic that allows one to state and prove relational properties of possibly infinite families of arbitrary programs. The key insights behind IRL are to (a) generalise relational program specifications in the style of Separation Logic triples to families of programs indexed by arbitrary infinite sets, and (b) provide general proof rules that support reasoning principles guided by the structure of these index sets. We have implemented IRL as a foundational embedding and verification tool on top of the Lean proof assistant. We demonstrate its power by showcasing both the practical and theoretical advances IRL brings to the state of the art in deductive program verification. To show the former, we use IRL to specify and prove the correctness of a series of previously unverified algorithms from computer graphics and geo-spatial information systems that iterate over array-encoded continuous objects. In doing so, we show that specifying representations of implicitly continuous data using code rather than traditional state invariants offers pragmatic benefits in the form of concise and reusable proofs, while retaining full compatibility with conventional non-relational Hoare-style reasoning. To show the latter, we use IRL to specify and verify a novel notion we call Weird Machine Realisability, providing the first conceptual framework that formally characterises the space of unintended behaviours permitted by a vulnerable program. All our case studies are formalised in Lean. |
|
| Gligoric, Milos |
Aditya Thimmaiah, Tong-Nong Lin, and Milos Gligoric (University of Texas at Austin, USA) |
|
| Goenka, Sneha |
Bala Vinaithirthan, Shiv Sundram, Sneha Goenka, and Fredrik Kjolstad (Stanford University, USA; Princeton University, USA) |
|
| Goharshady, Amir K. |
Amir K. Goharshady, Chun Kit Lam, Andreas Pavlogiannis, and Ahmed Khaled Zaher (Gran Sasso Science Institute, Italy; Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark) Minimizing code size is a central problem in compiler optimization, especially in the context of embedded systems and mobile applications. One of the classical optimizations that has recently been adopted to reduce the output code size is function inlining, i.e. repeatedly replacing a function call site by the body of the called function. At first glance, the fact that inlining can help reduce code size is counter-intuitive. However, it enables two types of subsequent optimizations which can affect the code size significantly: (i) the intra-procedural optimizations performed within each function, which make use of the additional context provided by inlining, and (ii) the elimination of dead functions. Many existing heuristics, such as those used by LLVM, focus on a local size analysis based on a few call sites. Thus, they miss the global opportunities to remove dead functions. On the other hand, the current state-of-the-art approach of auto-tuning by Theodoridis et al. [ASPLOS 2022] focuses on global code size but inspects each call site independently in order to avoid a combinatorial explosion. However, inlining decisions are not independent in practice. It is possible that two inlining choices each increase code size on their own, but applying both of them together reduces the size. In this work, we show that the problem of optimal inlining for code size minimization is NP-hard. We then present a completely different approach to this problem. Our algorithm is based on equality graphs (e-graphs), which are a standard tool in automated theorem proving and have recently been adopted by the compiler optimization community as a key ingredient in equality saturation. We show that optimal function inlining can be reduced to e-graph extraction. Although e-graph extraction is also NP-hard, there are efficient solvers that can handle sparse instances of this problem [OOPSLA 2024]. We build upon these solvers and add further inlining-specific heuristics to design an algorithm for code size reduction. Finally, we present experimental results on the standard SPEC benchmarks. Compared with LLVM, our approach reduces the code size to 95.34%. This is competitive with the state-of-the-art auto-tuning method of [ASPLOS 2022], which achieves 95.24%. In terms of running time, our approach is 20x faster than auto-tuning. More importantly, due to the two methods having orthogonal strengths, applying both of them leads to a further significant improvement, reducing the code size to 93.94% of LLVM's output. |
|
| Goldstein, Harrison |
Segev Elazar Mittelman, Harrison Goldstein, and Leonidas Lampropoulos (University of Maryland, College Park, USA; University at Buffalo, USA) |
|
| Gori, Roberta |
Roberto Bruni, Lorenzo Gazzella, and Roberta Gori (University of Pisa, Italy) |
|
| Graham, Kirsten |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Gray, Gavin |
Gavin Gray, Shriram Krishnamurthi, and Will Crichton (Brown University, USA) |
|
| Grosser, Tobias |
Siddharth Bhat, Léo Stefanesco, George Rennie, John Regehr, and Tobias Grosser (University of Cambridge, UK; University of Utah, USA) |
|
| Gu, Ronghui |
Wei Qiang and Ronghui Gu (Columbia University, USA; Certik, New York, USA) Yi Rong, Xupeng Li, and Ronghui Gu (Columbia University, USA; CertiK, USA) |
|
| Guo, Zihan |
Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, and Guoqiang Li (Shanghai Jiao Tong University, China; Chinese University of Hong Kong, Hong Kong; Shanghai University of Finance and Economics, China; Sun Yat-sen University, China) |
|
| Haas, Julian |
Julian Haas, Ragnar Mogk, Annette Bieniusa, and Mira Mezini (Technische Universität Darmstadt, Germany; Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Germany) |
|
| Havlík, Jakub |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| He, Yumeng |
Yumeng He and Pavel Panchekha (University of Utah, USA) |
|
| Hong, Jintai |
Li Lin, Jintai Hong, Yanlin Zhuang, and Rongxin Wu (Xiamen University, China) Mutation-based fuzzing is one of the most effective techniques for uncovering bugs in Database Management Systems (DBMSs). However, its effectiveness critically depends on the quality of the initial seed queries. High-quality seeds should be syntactically and semantically valid, incorporate diverse SQL features, and encode behaviors that drive execution into bug-prone states. In practice, existing DBMS fuzzers primarily rely on SQL queries extracted from unit tests or regression suites as initial seeds, which are often limited in diversity and scale, leaving many DBMS features and execution paths unexplored. To address this limitation, we propose SmartFuzz, an automated framework for synthesizing high-quality initial SQL seeds for mutation-based DBMS fuzzing using Large Language Models (LLMs). The key insight behind SmartFuzz is that two underutilized sources---official DBMS documentation and historical crash-triggering inputs---capture complementary knowledge about DBMS feature usage and bug-relevant behaviors. SmartFuzz extracts structured features from these sources and leverages LLMs to synthesize executable, feature-rich SQL seeds that are biased toward bug-prone execution states. We integrate SmartFuzz into existing mutation-based DBMS fuzzing pipelines and evaluate it on 4 widely used DBMSs. The results demonstrate that SmartFuzz significantly improves bug discovery and code coverage compared to state-of-the-art mutation-based fuzzers. In total, SmartFuzz detects 61 previously unknown bugs, of which 60 have been confirmed and fixed by developers. |
|
| Hong, Weijiang |
Yide Du, Zhenbang Chen, Weijiang Hong, and Wei Dong (National University of Defense Technology, China) |
|
| Horký, Vojtěch |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Huang, Heqing |
Heqing Huang and Zhendong Su (City University of Hong Kong, China; ETH Zurich, Switzerland) Path coverage tracing is one of the fundamental components for supporting a wide range of dynamic program analyses, such as testing, debugging, profiling, and many others. Since one needs to insert code into a program to trace its coverage, runtime overhead becomes the main bottleneck for scalability. As finding the minimum number of instrumentation points is NP-hard, extensive work has focused on reducing the number of instrumented edges under diverse assumptions, and thus suffers from the trade-off between precision and efficiency. Departing from this edge-centric view, we introduce, in this work, a novel perspective, namely the node-centric view, where we aim to find the minimum number of blocks, rather than edges as in existing work, that can differentiate all edges and paths in the program. This new perspective allows us to design a linear-time algorithm that is provably correct and optimal—it finds the minimum set of blocks for correctly differentiating edge/path coverage for arbitrary control-flow graphs. Our key insight is that optimal node-level instrumentation only needs to distinguish undifferentiated paths at the block where they converge, enabling our algorithm to have linear-time complexity regarding the number of basic blocks. We implement our algorithm as InsOpt and compare it against state-of-the-art edge-coverage instru- mentation techniques on the real-world vulnerability-detection benchmark, Magma. Our evaluation results demonstrate significant improvements: InsOpt needs 2.8x less instrumentation with only 17% basic blocks instrumented. This reduced instrumentation yields a 1.6x speedup and a substantial 2.4x reduction in runtime overhead. Moreover, we also demonstrate substantial potential for InsOpt across other applications. Specifically, our integration of InsOpt with AFL++, a state-of-the-art fuzzer, shows a 5.0x speedup in vulnerability detection and a 1.5x performance improvement. Notably, this efficiency gain further benefits InsOpt in detecting five previously unknown bugs in frequently evaluated projects by other state-of-the-art tools. |
|
| Huang, Jeff |
Yichuan Li, Wei Song, Jeff Huang, and Hans-Arno Jacobsen (Nanjing University of Science and Technology, China; Texas A&M University, USA; University of Toronto, Canada) Recovering the structure of a Solidity smart contract from its deployed bytecode is a prerequisite for various downstream analyses, such as control-flow graph construction, decompilation, and clone detection. A central step in this task is identifying private functions. However, since all source-level function boundaries are completely lost after compilation, the major challenge of this task lies in how to differentiate function calls from intra-procedural control transfers, because both are implemented via the JUMP/JUMPI instructions. We observe that although jump-based control transfers are superficially uniform, their context information is different. Some contexts provide definitive evidence of an intra-procedural control transfer or a function call, which inspires us to address this problem through progressive refinement rather than naive binary classification. Specifically, we first construct an over-approximated set of potential function call sites based on EVM execution semantics, and then narrow them down using rule-based reasoning. The remaining uncertain cases are finally resolved through probabilistic inference over suggestive contexts. For each identified function, we further analyze the instructions before each jump to determine its target and reassemble scattered code fragments into a continuous instruction sequence. We implement our approach as an open-source tool, dubbed ReFun, and evaluate it on 8,696 real-world Solidity smart contracts across multiple Solidity compiler versions and optimization settings. The experimental results demonstrate that ReFun achieves 94.3% precision and 95.5% recall in function recovery, and it is also efficient, completing function identification and separation for 82% of contracts within eight seconds per contract. Finally, we show how ReFun is applied to the downstream tasks, including contract decompilation and clone detection. |
|
| Huang, Peishan |
Peishan Huang, Wenmeng Zhang, Yusen Chen, and Zhenbang Chen (National University of Defense Technology, China) |
|
| Huang, Yifei |
Sara Baradaran, Yifei Huang, Wei Le, and Mukund Raghothaman (University of Southern California, USA; Iowa State University, USA) |
|
| Hublet, François |
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin (ETH Zurich, Switzerland) Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems. The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination. We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds. |
|
| Hunt, Guerney |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Huo, Wei |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Igarashi, Atsushi |
Yuito Murase and Atsushi Igarashi (Kyoto University, Japan) MetaML-style multi-stage programming (MSP) supports quasi-quotation-based code generation, runtime execution of generated code, and cross-stage persistence (CSP). However, its interaction with computational effects is subtle: mutable state can cause scope extrusion, where generated code escapes the scope of variables on which it depends. This paper presents a type system for MetaML-style MSP with mutable state that statically rules out harmful scope extrusion while supporting multi-level code generation, runtime execution, and a variant of CSP. Our system builds on refined environment classifiers (RECs), a discipline that annotates code types with the variable scopes on which generated code depends. To scale RECs to the MetaML-style setting, we refine classifiers so that they track not only variable scopes, but also the scopes of classifiers themselves. Further, we integrated polymorphism over classifiers, enabling more general and reusable code generation patterns in a multi-level setting. For the resulting system, we define an operational semantics via a definitional interpreter and prove type soundness and safety of offline code generation, showing that generated code can be extracted as standalone well-typed programs. We provide working implementations and mechanized proofs in Rocq. |
|
| Irmejs, Reinis |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Jacob, Dejice |
Xiaoyang Sun, Dejice Jacob, Huanting Wang, Jeremy Singer, and Zheng Wang (University of Leeds, UK; University of Glasgow, UK) Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions. |
|
| Jacobs, Jules |
Katherine Wu, Jules Jacobs, Kevin Batz, and Alexandra Silva (Cornell University, USA; Jane Street, USA) |
|
| Jacobsen, Hans-Arno |
Yichuan Li, Wei Song, Jeff Huang, and Hans-Arno Jacobsen (Nanjing University of Science and Technology, China; Texas A&M University, USA; University of Toronto, Canada) Recovering the structure of a Solidity smart contract from its deployed bytecode is a prerequisite for various downstream analyses, such as control-flow graph construction, decompilation, and clone detection. A central step in this task is identifying private functions. However, since all source-level function boundaries are completely lost after compilation, the major challenge of this task lies in how to differentiate function calls from intra-procedural control transfers, because both are implemented via the JUMP/JUMPI instructions. We observe that although jump-based control transfers are superficially uniform, their context information is different. Some contexts provide definitive evidence of an intra-procedural control transfer or a function call, which inspires us to address this problem through progressive refinement rather than naive binary classification. Specifically, we first construct an over-approximated set of potential function call sites based on EVM execution semantics, and then narrow them down using rule-based reasoning. The remaining uncertain cases are finally resolved through probabilistic inference over suggestive contexts. For each identified function, we further analyze the instructions before each jump to determine its target and reassemble scattered code fragments into a continuous instruction sequence. We implement our approach as an open-source tool, dubbed ReFun, and evaluate it on 8,696 real-world Solidity smart contracts across multiple Solidity compiler versions and optimization settings. The experimental results demonstrate that ReFun achieves 94.3% precision and 95.5% recall in function recovery, and it is also efficient, completing function identification and separation for 82% of contracts within eight seconds per contract. Finally, we show how ReFun is applied to the downstream tasks, including contract decompilation and clone detection. |
|
| Jagadeesan, Radha |
Samson Abramsky and Radha Jagadeesan (University College London, UK; DePaul University, USA) Existing quantum programming languages confine higher-order structure to a classical host while restricting the quantum layer to first-order operations on qubits. This paper presents Granthi, a purely unitary higher-order quantum programming language built on three design commitments: quantum programs are first-class values that may be passed, returned, and coherently composed; additive structure is tag-preserving routing rather than observational branching, so control may remain in superposition; and programmer-facing finite label types with named reversible operations provide domain-level control spaces without exposing tag management. Every well-typed term—including at function type—denotes a unitary on its boundary interface, and the compiler realizes exactly its wiring as a quantum circuit on the physical qubit layout (assuming correctness of the pytket backend). Granthi is implemented end-to-end: an OCaml DSL elaborates surface programs through a binder-free core IR to executable quantum circuits via pytket. The language directly supports the quantum switch—the paper’s running example, compiled to a static circuit—as well as interference on control-flow history and structured finite control, all within the purely unitary fragment. |
|
| Jain, Devansh |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Jakubovic, Joel |
Joel Jakubovic (Charles University, Czech Republic) |
|
| Jeannin, Jean-Baptiste |
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin (University of Michigan, USA; Shanghai University of Finance and Economics, China) Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art. |
|
| Jeon, Jonguk |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. |
|
| Jeon, Seungmin |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. |
|
| Jeong, Seokhun |
Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu (KAIST, Republic of Korea) Programming languages evolve over time, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, like JavaScript and WebAssembly (Wasm), keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and Wasm specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. Both framework designs leverage the existence of JavaScript and Wasm’s normative specifications, which is not the case for many languages. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 is a statically-typed domain-specific language for programming packet processors. It is evolving without a normative specification, thereby introducing inconsistencies and errors into the P4 ecosystem. From a mechanization framework perspective, P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain. We share the lessons learned from our case study, to provide insights for integrating mechanization into real-world languages without normative specifications. |
|
| Jia, Fuqi |
Maolin Sun, Fuqi Jia, Yibiao Yang, and Yuming Zhou (Nanjing University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by integrating logical reasoning with numerical optimization to address constrained optimization problems across diverse theories. Optimizing SMT solvers (also known as OMT solvers), designed to handle such problems, serve as foundational components in numerous applications within programming languages research and practice. However, despite their widespread adoption, OMT solvers are susceptible to subtle yet critical bugs that can silently mislead downstream applications by providing incorrect optimal solutions, potentially leading to severe consequences. Validating these solvers poses a fundamental challenge, as obtaining precise ground truth for optimal solutions is inherently difficult, particularly under complex or theory-specific objective functions. Moreover, existing SMT solver testing techniques are inadequate, as they fail to capture the intricate interplay between satisfiability checking and optimization reasoning in OMT. To overcome these challenges, we propose cross-theory approximation, a novel validation methodology that leverages the relationships between solution spaces of different logical theories. The key insight is that an optimal solution produced in one theory should maintain expected relationships when interpreted in another comparable theory's solution space. By defining these cross-theory consistency properties and comparing optimal solutions obtained through theory-specific transformations, we can detect discrepancies that indicate potential solver bugs. For instance, an integer-optimal solution should map cleanly into the broader real-arithmetic domain; deviations from this expected relationship signal incorrect optimization behavior. We implement this methodology in Iris, a practical framework for validating OMT solvers. When testing on the advanced OMT solvers, including Z3 and OptiMathSAT, Iris uncovers 24 previously unknown bugs, 20 of which were subsequently resolved by developers. Notably, most of our reported bugs are correctness issues, emphasizing the effectiveness of our approach in enhancing OMT solver reliability. |
|
| Jiang, Anxiao |
Dat Nguyen, Vasudha Devarakonda, Anxiao Jiang, and Khanh Nguyen (Texas A&M University, USA) |
|
| Kalita, Pankaj Kumar |
Gourav Takhar, Sumit Lahiri, Pankaj Kumar Kalita, and Subhajit Roy (IIT Kanpur, India; Qualcomm, India; IBM Research, India) Modern software systems routinely invoke components whose source code is unavailable, such as proprietary libraries or cloud-based APIs. Such closed-box functions provide only oracle-style access: they can be executed on concrete inputs, but their internal logic cannot be inspected. Prior work has explored augmenting SMT solvers—the foundational engines behind contemporary automated reasoning—to handle satisfiability queries over first-order formulas containing calls to such closed-box functions. However, these approaches primarily rely on testing-based techniques to search for satisfying models and therefore do not support constructing proofs of unsatisfiability. While model search is sufficient for bug-finding tasks, the inability to generate unsatisfiability proofs fundamentally limits their applicability to formal verification. In this work, we present the first SMT solver capable of producing proofs of unsatisfiability for first-order theories that include closed-box function calls. Our key insight is to leverage large language models (LLMs) to conjecture auxiliary lemmas—based on natural language documentation of the closed-box functions—that capture properties relevant for reasoning about their behavior. To support this approach, we introduce an extension of the SMT-LIB language that allows the declaration of closed-box functions together with natural language descriptions, usage documentation, examples, and oracle interfaces. We, then, develop NLUnsat, an SMT solver that operates over this extended syntax to find unsatisfiability proofs on SMT-LIB formulas with closed-box functions. On a benchmark suite of 193 extended SMT-LIB problems involving closed-box functions, NLUnsat equipped with the openai.gpt-oss:20b LLM solves 89% of the instances, and a virtual best solver across five LLMs solves 98% of the instances. We further evaluate NLUnsat in the setting of deductive verification for programs containing closed-box function calls. On a collection of 15 benchmark programs, our verifier, using NLUnsat as its backend solver, successfully proves all verification goals when given access to a pool of two LLMs, openai.gpt-oss:20b and openai.gpt-oss:120b. Finally, we evaluate NLUnsat on satisfiable benchmark instances: none of these instances were incorrectly classified as unsatisfiable, and the solver successfully finds models for 57 out of 107 satisfiable instances. |
|
| Kamina, Tetsuo |
Tomoyuki Aotani and Tetsuo Kamina (Sanyo-Onoda City University, Japan; Oita University, Japan) |
|
| Kang, Jeehoon |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. |
|
| Kayal, Neeraj |
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India; Google DeepMind, India) |
|
| Kehrli, Sascha |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Khan, Mikail |
Dinghong Zhong, Alexander Y. Bai, Mikail Khan, and Guannan Wei (Tufts University, USA; New York University, USA; Carnegie Mellon University, USA) |
|
| Khulbe, Kaustubh |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Kim, Jinwoo |
Jinwoo Kim, Victor Nicolet, Joey Dodds, and Loris D'Antoni (University of California at San Diego, USA; Amazon, USA) |
|
| Kiser, Matthew |
Armando Bellante, Reinis Irmejs, Marta Florido-Llinàs, María Cea Fernández, Marianna Crupi, Matthew Kiser, and J. Ignacio Cirac (Max Planck Institute of Quantum Optics, Germany; Munich Center for Quantum Science and Technology, Germany; TU Munich, Germany; IQM Quantum Computers, Germany) State preparation compilers for quantum computers typically sit at two extremes: general-purpose routines that treat the target as an opaque amplitude vector, and bespoke constructions for a handful of well-known state families. We ask whether a compiler can instead accept simple, structure-aware specifications while providing predictable resource guarantees. We answer this by designing and implementing a quantum state-preparation compiler for regular language states (RLS): uniform superpositions over bitstrings accepted by a regular description, and their complements. Users describe the target state via (i) a finite set of bitstrings, (ii) a regular expression, or (iii) a deterministic finite automaton (DFA), optionally with a complement flag. By translating the input to a DFA, minimizing it, and mapping it to an optimal matrix product state (MPS), the compiler obtains an intermediate representation (IR) that exposes and compresses hidden structure. The efficient DFA representation and minimization offloads expensive linear algebra computation in exchange of simpler automata manipulations. The combination of the regular-language frontend and this IR gives concise specifications not only for RLS but also for their complements that might otherwise require exponentially large state descriptions. This enables state preparation of an RLS or its complement with the same asymptotic resources and compile time, which to our knowledge is not supported by existing compilers. We outline two hardware-aware backends: SeqRLSP, which yields linear-depth, ancilla-free circuits for linear nearest-neighbor architectures via sequential generation, and TreeRLSP, which achieves logarithmic depth on all-to-all connectivity via a tree tensor network. On the theory side, we prove circuit-depth and gate-count bounds that scale with the system size and the maximal Schmidt rank of the target state, and we give compile-time bounds that expose the benefit of the initial DFA representation. We implement the full pipeline and evaluate it on Dicke and W states, random uniform superpositions, and complement states, comparing against general-purpose, sparse-state, and specialized baselines. |
|
| Kissinger, Aleks |
Ben Caldwell, William Spencer, Aleks Kissinger, and Robert Rand (University of Chicago, USA; University of Oxford, UK) Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition obscures the essential connective information, leading to longer proofs filled with syntactic manipulation. To address the gap between proof assistants and paper proofs, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning over these systems. Our tactics can also be used in existing verification projects about symmetric monoidal categories that can be treated as tensors. |
|
| Kjolstad, Fredrik |
Bala Vinaithirthan, Shiv Sundram, Sneha Goenka, and Fredrik Kjolstad (Stanford University, USA; Princeton University, USA) |
|
| Klose, Nicolas |
Nicolas Klose and Peter Müller (ETH Zurich, Switzerland) |
|
| Kokologiannakis, Michalis |
Azalea Raad, Michalis Kokologiannakis, Viktor Vafeiadis, and Conrad Watt (Imperial College London, UK; ETH Zurich, Switzerland; MPI-SWS, Germany; Nanyang Technological University, Singapore) |
|
| Křikava, Filip |
Mickaël Laurent, Pierre Donat-Bouillud, Filip Křikava, and Jan Vitek (Charles University, Czech Republic; Czech Technical University, Czech Republic) Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple---a row variable maps to a single row---and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch. |
|
| Krishnamurthi, Shriram |
Gavin Gray, Shriram Krishnamurthi, and Will Crichton (Brown University, USA) |
|
| Krstić, Srđan |
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin (ETH Zurich, Switzerland) Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems. The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination. We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds. |
|
| Kulkarni, Bhargav |
Bhargav Kulkarni, Henry Whiting, and Pavel Panchekha (University of Utah, USA) |
|
| Kunčak, Viktor |
Matt Bovel, Viktor Kunčak, and Martin Odersky (EPFL, Switzerland) |
|
| Kwon, Haechan |
Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu (KAIST, Republic of Korea) Programming languages evolve over time, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, like JavaScript and WebAssembly (Wasm), keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and Wasm specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. Both framework designs leverage the existence of JavaScript and Wasm’s normative specifications, which is not the case for many languages. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 is a statically-typed domain-specific language for programming packet processors. It is evolving without a normative specification, thereby introducing inconsistencies and errors into the P4 ecosystem. From a mechanization framework perspective, P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain. We share the lessons learned from our case study, to provide insights for integrating mechanization into real-world languages without normative specifications. |
|
| Laeufer, Kevin |
Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, and Adrian Sampson (Cornell University, USA) |
|
| Lafeychine, Vincent |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Lahiri, Sumit |
Gourav Takhar, Sumit Lahiri, Pankaj Kumar Kalita, and Subhajit Roy (IIT Kanpur, India; Qualcomm, India; IBM Research, India) Modern software systems routinely invoke components whose source code is unavailable, such as proprietary libraries or cloud-based APIs. Such closed-box functions provide only oracle-style access: they can be executed on concrete inputs, but their internal logic cannot be inspected. Prior work has explored augmenting SMT solvers—the foundational engines behind contemporary automated reasoning—to handle satisfiability queries over first-order formulas containing calls to such closed-box functions. However, these approaches primarily rely on testing-based techniques to search for satisfying models and therefore do not support constructing proofs of unsatisfiability. While model search is sufficient for bug-finding tasks, the inability to generate unsatisfiability proofs fundamentally limits their applicability to formal verification. In this work, we present the first SMT solver capable of producing proofs of unsatisfiability for first-order theories that include closed-box function calls. Our key insight is to leverage large language models (LLMs) to conjecture auxiliary lemmas—based on natural language documentation of the closed-box functions—that capture properties relevant for reasoning about their behavior. To support this approach, we introduce an extension of the SMT-LIB language that allows the declaration of closed-box functions together with natural language descriptions, usage documentation, examples, and oracle interfaces. We, then, develop NLUnsat, an SMT solver that operates over this extended syntax to find unsatisfiability proofs on SMT-LIB formulas with closed-box functions. On a benchmark suite of 193 extended SMT-LIB problems involving closed-box functions, NLUnsat equipped with the openai.gpt-oss:20b LLM solves 89% of the instances, and a virtual best solver across five LLMs solves 98% of the instances. We further evaluate NLUnsat in the setting of deductive verification for programs containing closed-box function calls. On a collection of 15 benchmark programs, our verifier, using NLUnsat as its backend solver, successfully proves all verification goals when given access to a pool of two LLMs, openai.gpt-oss:20b and openai.gpt-oss:120b. Finally, we evaluate NLUnsat on satisfiable benchmark instances: none of these instances were incorrectly classified as unsatisfiable, and the solver successfully finds models for 57 out of 107 satisfiable instances. |
|
| Lam, Chun Kit |
Amir K. Goharshady, Chun Kit Lam, Andreas Pavlogiannis, and Ahmed Khaled Zaher (Gran Sasso Science Institute, Italy; Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark) Minimizing code size is a central problem in compiler optimization, especially in the context of embedded systems and mobile applications. One of the classical optimizations that has recently been adopted to reduce the output code size is function inlining, i.e. repeatedly replacing a function call site by the body of the called function. At first glance, the fact that inlining can help reduce code size is counter-intuitive. However, it enables two types of subsequent optimizations which can affect the code size significantly: (i) the intra-procedural optimizations performed within each function, which make use of the additional context provided by inlining, and (ii) the elimination of dead functions. Many existing heuristics, such as those used by LLVM, focus on a local size analysis based on a few call sites. Thus, they miss the global opportunities to remove dead functions. On the other hand, the current state-of-the-art approach of auto-tuning by Theodoridis et al. [ASPLOS 2022] focuses on global code size but inspects each call site independently in order to avoid a combinatorial explosion. However, inlining decisions are not independent in practice. It is possible that two inlining choices each increase code size on their own, but applying both of them together reduces the size. In this work, we show that the problem of optimal inlining for code size minimization is NP-hard. We then present a completely different approach to this problem. Our algorithm is based on equality graphs (e-graphs), which are a standard tool in automated theorem proving and have recently been adopted by the compiler optimization community as a key ingredient in equality saturation. We show that optimal function inlining can be reduced to e-graph extraction. Although e-graph extraction is also NP-hard, there are efficient solvers that can handle sparse instances of this problem [OOPSLA 2024]. We build upon these solvers and add further inlining-specific heuristics to design an algorithm for code size reduction. Finally, we present experimental results on the standard SPEC benchmarks. Compared with LLVM, our approach reduces the code size to 95.34%. This is competitive with the state-of-the-art auto-tuning method of [ASPLOS 2022], which achieves 95.24%. In terms of running time, our approach is 20x faster than auto-tuning. More importantly, due to the two methods having orthogonal strengths, applying both of them leads to a further significant improvement, reducing the code size to 93.94% of LLVM's output. |
|
| Lampropoulos, Leonidas |
Segev Elazar Mittelman, Harrison Goldstein, and Leonidas Lampropoulos (University of Maryland, College Park, USA; University at Buffalo, USA) |
|
| Larsen, Andreas Stenbæk |
Magnus Madsen, Andreas Stenbæk Larsen, Jakob Schneider Villumsen, and Aslan Askarov (Aarhus University, Denmark) Today, most software is developed by building on packages, allowing developers to accelerate development. The proliferation of package dependencies creates a target-rich environment for malicious actors to hijack packages to inject malware, steal sensitive information, or cause destruction. Such supply chain attacks constantly threaten package ecosystems such as Cargo, npm, and Maven. In this paper, we explore how to fight against such attacks by leveraging effect systems. While effect systems predict the behavior of software components, there is a practical gap between a programming language with an effect system and a programming language ecosystem that can use such effects to thwart attacks. To close this gap, we introduce a notion of an effect-safe package upgrade and develop an effect-aware package manager that enforces safety through effect lock files. We extend the Flix programming language and its compiler toolchain with an effect-aware package manager. We evaluate the usefulness of the proposed effect-aware package manager with a case study of 51 supply chain attacks from the "Backstabbers Knife Collection" corpus of malware. The study suggests that 48 of these attacks are likely preventable with our proposed effect-aware package manager. |
|
| Laurent, Mickaël |
Mickaël Laurent and Kim Nguyễn (Charles University, Czech Republic; Université Paris-Saclay, France) Set-theoretic types provide a rich type algebra that supports unrestricted unions, intersections, and negations, together with a decidable type constraint-solving algorithm known as tallying. These types are particularly well suited for typing dynamic languages, where functions often exhibit both generic and overloaded behavior. However, the complexity of their implementation has hindered their widespread adoption. In this paper, we introduce a modular representation for set-theoretic types and revisit the algorithms for subtyping and tallying. We compare our approach with the historical CDuce implementation and evaluate the performance impact of some optimizations and design choices. Mickaël Laurent, Pierre Donat-Bouillud, Filip Křikava, and Jan Vitek (Charles University, Czech Republic; Czech Technical University, Czech Republic) Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple---a row variable maps to a single row---and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch. |
|
| Le, Wei |
Sara Baradaran, Yifei Huang, Wei Le, and Mukund Raghothaman (University of Southern California, USA; Iowa State University, USA) |
|
| Lee, Jaehyun |
Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu (KAIST, Republic of Korea) Programming languages evolve over time, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, like JavaScript and WebAssembly (Wasm), keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and Wasm specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. Both framework designs leverage the existence of JavaScript and Wasm’s normative specifications, which is not the case for many languages. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 is a statically-typed domain-specific language for programming packet processors. It is evolving without a normative specification, thereby introducing inconsistencies and errors into the P4 ecosystem. From a mechanization framework perspective, P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain. We share the lessons learned from our case study, to provide insights for integrating mechanization into real-world languages without normative specifications. |
|
| Lee, Kanguk |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. |
|
| Lemerre, Matthieu |
Julien Simonnet, Matthieu Lemerre, and Mihaela Sighireanu (Université Paris-Saclay - CEA LIST, France; Université Paris-Saclay - ENS Paris-Saclay - CNRS - LMF, France) Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose relations, while assignment-based relational designs capture relations but hinder modularity and reuse. We introduce open lattices and abstract abstract datatypes (AADT), a new foundation for building precise and reusable abstract domains for structured values. Open lattices generalize classical lattices by introducing shared symbolic values constrained by an abstract valuation domain, enabling relational reasoning across independently defined abstractions. AADTs are compositional transformers over open lattices that mirror the structure of concrete data types: addresses, records, unions, variants, arrays, and their arbitrary nesting. Because each AADT closely follows the concrete datatype definition, abstract domain operations are modular and easy to reuse or extend. Most AADT transformers that we provide are exact: when the abstract valuation domain is exact, the resulting abstraction is a precise translation of the concrete semantics. This enables applications beyond static analysis, such as counter-example generation. We formalize open lattices and AADTs, present key instances, and implement them in a framework for the analysis of C and binary programs. Our experiments show precision gains over state-of-the-art abstract interpreters, while maintaining comparable analysis times. |
|
| Lengál, Ondřej |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| Li, Guoqiang |
Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, and Guoqiang Li (Shanghai Jiao Tong University, China; Chinese University of Hong Kong, Hong Kong; Shanghai University of Finance and Economics, China; Sun Yat-sen University, China) |
|
| Li, Xitao |
Xitao Li, Xiaofei Xie, Jiang Wu, Ting Liu, and Haijun Wang (Xi'an Jiaotong University, China; Singapore Management University, Singapore) |
|
| Li, Xupeng |
Yi Rong, Xupeng Li, and Ronghui Gu (Columbia University, USA; CertiK, USA) |
|
| Li, Yeting |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Li, Yichuan |
Yichuan Li, Wei Song, Jeff Huang, and Hans-Arno Jacobsen (Nanjing University of Science and Technology, China; Texas A&M University, USA; University of Toronto, Canada) Recovering the structure of a Solidity smart contract from its deployed bytecode is a prerequisite for various downstream analyses, such as control-flow graph construction, decompilation, and clone detection. A central step in this task is identifying private functions. However, since all source-level function boundaries are completely lost after compilation, the major challenge of this task lies in how to differentiate function calls from intra-procedural control transfers, because both are implemented via the JUMP/JUMPI instructions. We observe that although jump-based control transfers are superficially uniform, their context information is different. Some contexts provide definitive evidence of an intra-procedural control transfer or a function call, which inspires us to address this problem through progressive refinement rather than naive binary classification. Specifically, we first construct an over-approximated set of potential function call sites based on EVM execution semantics, and then narrow them down using rule-based reasoning. The remaining uncertain cases are finally resolved through probabilistic inference over suggestive contexts. For each identified function, we further analyze the instructions before each jump to determine its target and reassemble scattered code fragments into a continuous instruction sequence. We implement our approach as an open-source tool, dubbed ReFun, and evaluate it on 8,696 real-world Solidity smart contracts across multiple Solidity compiler versions and optimization settings. The experimental results demonstrate that ReFun achieves 94.3% precision and 95.5% recall in function recovery, and it is also efficient, completing function identification and separation for 82% of contracts within eight seconds per contract. Finally, we show how ReFun is applied to the downstream tasks, including contract decompilation and clone detection. |
|
| Li, Yue |
Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li (Nanjing University, China) Heap abstraction critically affects both the efficiency and precision of pointer analysis for Java programs. By merging heap objects allocated at different program points, heap abstractions can significantly improve analysis efficiency, but often at the cost of precision. Mahjong, a state-of-the-art heap abstraction based on object merging, demonstrates that object merging can substantially improve the efficiency of pointer analysis while preserving precision for type-dependent clients; however, this client-specific guarantee limits its general applicability. In this work, we investigate how to improve the efficiency of pointer analysis through object merging, while preserving precision in a manner independent of any particular client. Our key insight is that, from the perspective of pointer analysis, many heap objects exhibit early flow confluence: they are allocated at different program points and then quickly propagate to the same pointers (variables or fields), after which they continue to flow together through the program. Merging such early-confluent objects has negligible impact on overall analysis precision. In contrast, merging objects that do not flow to the same pointers, or that converge only much later, can introduce substantial precision loss. Guided by this insight, we propose Valve, a new heap abstraction approach that efficiently identifies and merges early-confluent objects. Valve encodes the flow information needed for early-confluence detection as nondeterministic finite automata (NFAs) and approximates mergeability checking via an NFA-equivalence test, enabling efficient object merging while retaining high precision. We evaluate Valve on the largest benchmarks used in recent literature as well as modern large-scale Java applications, by integrating it with multiple state-of-the-art pointer-analysis techniques and directly comparing it with Mahjong. The results show that Valve achieves substantially higher precision than Mahjong for non-type-dependent clients, while maintaining comparable precision for type-dependent clients. At the same time, Valve delivers comparable or often better analysis efficiency across all evaluated cases. Overall, Valve, as a heap abstraction approach, significantly improves the efficiency of pointer analysis across several state-of-the-art techniques while maintaining high precision (99.61% on average). Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. |
|
| Li, Zenan |
Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma (Nanjing University, China; ETH Zurich, Switzerland) As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either. |
|
| Liang, Sijie |
Yihan Dai, Sijie Liang, Haotian Xu, Peichu Xie, and Sergey Mechtaev (Peking University, China; Beijing Forestry University, China; Independent, China) |
|
| Liang, Yufei |
Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li (Nanjing University, China) Heap abstraction critically affects both the efficiency and precision of pointer analysis for Java programs. By merging heap objects allocated at different program points, heap abstractions can significantly improve analysis efficiency, but often at the cost of precision. Mahjong, a state-of-the-art heap abstraction based on object merging, demonstrates that object merging can substantially improve the efficiency of pointer analysis while preserving precision for type-dependent clients; however, this client-specific guarantee limits its general applicability. In this work, we investigate how to improve the efficiency of pointer analysis through object merging, while preserving precision in a manner independent of any particular client. Our key insight is that, from the perspective of pointer analysis, many heap objects exhibit early flow confluence: they are allocated at different program points and then quickly propagate to the same pointers (variables or fields), after which they continue to flow together through the program. Merging such early-confluent objects has negligible impact on overall analysis precision. In contrast, merging objects that do not flow to the same pointers, or that converge only much later, can introduce substantial precision loss. Guided by this insight, we propose Valve, a new heap abstraction approach that efficiently identifies and merges early-confluent objects. Valve encodes the flow information needed for early-confluence detection as nondeterministic finite automata (NFAs) and approximates mergeability checking via an NFA-equivalence test, enabling efficient object merging while retaining high precision. We evaluate Valve on the largest benchmarks used in recent literature as well as modern large-scale Java applications, by integrating it with multiple state-of-the-art pointer-analysis techniques and directly comparing it with Mahjong. The results show that Valve achieves substantially higher precision than Mahjong for non-type-dependent clients, while maintaining comparable precision for type-dependent clients. At the same time, Valve delivers comparable or often better analysis efficiency across all evaluated cases. Overall, Valve, as a heap abstraction approach, significantly improves the efficiency of pointer analysis across several state-of-the-art techniques while maintaining high precision (99.61% on average). |
|
| Lin, Haoran |
Yifan Zhang, Yuanfeng Shi, Haoran Lin, Yingfei Xiong, and Xin Zhang (Peking University, China) |
|
| Lin, Jyun-Ao |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| Lin, Li |
Li Lin, Jintai Hong, Yanlin Zhuang, and Rongxin Wu (Xiamen University, China) Mutation-based fuzzing is one of the most effective techniques for uncovering bugs in Database Management Systems (DBMSs). However, its effectiveness critically depends on the quality of the initial seed queries. High-quality seeds should be syntactically and semantically valid, incorporate diverse SQL features, and encode behaviors that drive execution into bug-prone states. In practice, existing DBMS fuzzers primarily rely on SQL queries extracted from unit tests or regression suites as initial seeds, which are often limited in diversity and scale, leaving many DBMS features and execution paths unexplored. To address this limitation, we propose SmartFuzz, an automated framework for synthesizing high-quality initial SQL seeds for mutation-based DBMS fuzzing using Large Language Models (LLMs). The key insight behind SmartFuzz is that two underutilized sources---official DBMS documentation and historical crash-triggering inputs---capture complementary knowledge about DBMS feature usage and bug-relevant behaviors. SmartFuzz extracts structured features from these sources and leverages LLMs to synthesize executable, feature-rich SQL seeds that are biased toward bug-prone execution states. We integrate SmartFuzz into existing mutation-based DBMS fuzzing pipelines and evaluate it on 4 widely used DBMSs. The results demonstrate that SmartFuzz significantly improves bug discovery and code coverage compared to state-of-the-art mutation-based fuzzers. In total, SmartFuzz detects 61 previously unknown bugs, of which 60 have been confirmed and fixed by developers. |
|
| Lin, Tong-Nong |
Aditya Thimmaiah, Tong-Nong Lin, and Milos Gligoric (University of Texas at Austin, USA) |
|
| Ling, Hongyi |
Hongyi Ling, Thibault Dardinier, Ellen Arlt, and Peter Müller (ETH Zurich, Switzerland; EPFL, Switzerland; MPI-SWS, Germany) Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL. |
|
| Ling, Yuxi |
Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey (National University of Singapore, Singapore; Princeton University, USA) Relational program logics are a popular formalism for stating and proving properties that relate executions of several computations. We present Infinitary Relational Logic (IRL)—the first Hoare-style Separation Logic that allows one to state and prove relational properties of possibly infinite families of arbitrary programs. The key insights behind IRL are to (a) generalise relational program specifications in the style of Separation Logic triples to families of programs indexed by arbitrary infinite sets, and (b) provide general proof rules that support reasoning principles guided by the structure of these index sets. We have implemented IRL as a foundational embedding and verification tool on top of the Lean proof assistant. We demonstrate its power by showcasing both the practical and theoretical advances IRL brings to the state of the art in deductive program verification. To show the former, we use IRL to specify and prove the correctness of a series of previously unverified algorithms from computer graphics and geo-spatial information systems that iterate over array-encoded continuous objects. In doing so, we show that specifying representations of implicitly continuous data using code rather than traditional state invariants offers pragmatic benefits in the form of concise and reusable proofs, while retaining full compatibility with conventional non-relational Hoare-style reasoning. To show the latter, we use IRL to specify and verify a novel notion we call Weird Machine Realisability, providing the first conceptual framework that formally characterises the space of unintended behaviours permitted by a vulnerable program. All our case studies are formalised in Lean. |
|
| Liu, Chengyue |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Liu, Chenke |
Chenke Liu, Li Zhou, and Boning Meng (Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) |
|
| Liu, Qikang |
Xiaoyu Liu, Qikang Liu, Evan Dyce, Keval Vora, and Yuepeng Wang (Simon Fraser University, Canada) Writing graph queries is challenging for non-experts due to the complexity of graph data models and the need to identify proper graph patterns. While recent research has advanced query synthesis for relational and document databases, the problem of synthesizing graph queries remains under-explored. We present a novel approach for synthesizing graph queries from computation demonstrations, where users specify the desired output through expressions over properties of input graphs. Our method addresses the challenge of inferring meaningful graph patterns for matching and efficiently constructing the remaining components of the query. Specifically, we combine graph mining, which identifies candidate patterns across input graphs, with deduction-based pruning, which guides an efficient synthesis of the filtering predicate and return clause. We have implemented our approach in a tool called DMiner and evaluated it on 90 benchmarks. Experimental results show that DMiner successfully synthesizes desired queries for 87 benchmarks, with an average synthesis time of 0.6 seconds per query. This outperforms both enumerative search and LLM baselines. We also conducted a user study, which shows that users can provide demonstrations with modest effort and 87.5% of the provided demonstrations are sufficient for DMiner to synthesize the desired query. |
|
| Liu, Ting |
Xitao Li, Xiaofei Xie, Jiang Wu, Ting Liu, and Haijun Wang (Xi'an Jiaotong University, China; Singapore Management University, Singapore) |
|
| Liu, Xiaoyu |
Xiaoyu Liu, Qikang Liu, Evan Dyce, Keval Vora, and Yuepeng Wang (Simon Fraser University, Canada) Writing graph queries is challenging for non-experts due to the complexity of graph data models and the need to identify proper graph patterns. While recent research has advanced query synthesis for relational and document databases, the problem of synthesizing graph queries remains under-explored. We present a novel approach for synthesizing graph queries from computation demonstrations, where users specify the desired output through expressions over properties of input graphs. Our method addresses the challenge of inferring meaningful graph patterns for matching and efficiently constructing the remaining components of the query. Specifically, we combine graph mining, which identifies candidate patterns across input graphs, with deduction-based pruning, which guides an efficient synthesis of the filtering predicate and return clause. We have implemented our approach in a tool called DMiner and evaluated it on 90 benchmarks. Experimental results show that DMiner successfully synthesizes desired queries for 87 benchmarks, with an average synthesis time of 0.6 seconds per query. This outperforms both enumerative search and LLM baselines. We also conducted a user study, which shows that users can provide demonstrations with modest effort and 87.5% of the provided demonstrations are sufficient for DMiner to synthesize the desired query. |
|
| Liu, Yang |
Lyuye Zhang, He Ye, Federica Sarro, Yuqiang Sun, and Yang Liu (Nankai University, China; Nanyang Technological University, Singapore; University College London, UK) Remediating vulnerabilities in open-source software (OSS) dependencies is vital to maintaining software supply chain security. However, current automated approaches almost exclusively rely on dependency upgrades, which is limited by the nature of upgrades, i.e., the availability of secure versions, version pinning, and API incompatibilities. To address the limitation, this paper presents Remedius, an agent-based remediation framework for Maven projects that unifies dependency upgrading and patch porting within a holistic optimization workflow. Remedius dynamically clusters dependencies by usage, gathers project-specific evidence through autonomous LLM-driven agents, and formulates a cost-aware remediation optimization problem solved via Satisfiability Modulo Theory (SMT). The agents translate complex contextual factors—such as compatibility, reachability, and patch difficulty—into solver-ready constraints, enabling flexible and scalable decision-making beyond what static rules or LLM reasoning alone can achieve. By redefining optimization at the vulnerability level rather than the dependency level, Remedius maximizes vulnerability coverage while preserving build correctness and runtime compatibility. An evaluation of 301 real-world Maven projects demonstrates that Remedius outperforms state-of-the-art baselines, achieving the highest number of vulnerabilities fixed and the fewest build or test failures. These results highlight a new direction for automated OSS remediation beyond upgrade-only solutions toward adaptive, agent-driven vulnerability management. Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Liu, Zhaoxiang |
Zhaoxiang Liu, James Parker, and Ning Luo (Kansas State University, USA; Ossa Network, USA; University of Illinois at Urbana-Champaign, USA) |
|
| Lo, Fang-Yi |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| Lochan, Saatvik |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Löff, Júnior |
Júnior Löff, Daniele Bonetta, and Walter Binder (USI Lugano, Switzerland; VU Amsterdam, Netherlands) Strings are the primary mechanism through which Java applications ingest external textual data, including data read from files, databases, network interfaces, and native libraries. In data-intensive applications, such data must either be materialized as heap-allocated java.lang.String objects, incurring allocation, copying, encoding, and garbage-collection costs, or accessed through low-level and unsafe foreign-memory mechanisms that require non-standard string APIs and explicit reasoning about memory management and object lifetimes. Neither option is well suited to high-volume ingestion workloads that require both efficiency and seamless integration with existing Java code. We present TwinString, an alternative representation of java.lang.String that decouples string semantics from the physical placement of its contents. A TwinString stores its data outside the regular Java heap while preserving the standard String type and behavior expected by Java programs and libraries. VM support controls this data and manages its lifetime with garbage collection, allowing foreign textual data to be exposed as ordinary strings without introducing additional custom string types. We implement TwinStrings in GraalVM Native Image and evaluate them across several workloads, including microbenchmarks, text-processing applications over real-world datasets, and data-heavy applications using JDBC and SQLite. The results show that TwinStrings significantly reduce allocation overhead while remaining compatible with the original String API, and reduce P99.9 tail latency by up to 42.2% in realistic library and JDBC workloads by alleviating heap allocation and garbage-collection pressure. |
|
| Lubin, Justin |
Parker Ziegler, David Minh-Duy Cao, Justin Lubin, and Sarah E. Chasins (University of California at Berkeley, USA) |
|
| Luo, Baoyuan |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Luo, Ning |
Zhaoxiang Liu, James Parker, and Ning Luo (Kansas State University, USA; Ossa Network, USA; University of Illinois at Urbana-Champaign, USA) |
|
| Ma, Xiaoxing |
Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma (Nanjing University, China; ETH Zurich, Switzerland) As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either. |
|
| Madsen, Magnus |
Magnus Madsen, Andreas Stenbæk Larsen, Jakob Schneider Villumsen, and Aslan Askarov (Aarhus University, Denmark) Today, most software is developed by building on packages, allowing developers to accelerate development. The proliferation of package dependencies creates a target-rich environment for malicious actors to hijack packages to inject malware, steal sensitive information, or cause destruction. Such supply chain attacks constantly threaten package ecosystems such as Cargo, npm, and Maven. In this paper, we explore how to fight against such attacks by leveraging effect systems. While effect systems predict the behavior of software components, there is a practical gap between a programming language with an effect system and a programming language ecosystem that can use such effects to thwart attacks. To close this gap, we introduce a notion of an effect-safe package upgrade and develop an effect-aware package manager that enforces safety through effect lock files. We extend the Flix programming language and its compiler toolchain with an effect-aware package manager. We evaluate the usefulness of the proposed effect-aware package manager with a case study of 51 supply chain attacks from the "Backstabbers Knife Collection" corpus of malware. The study suggests that 48 of these attacks are likely preventable with our proposed effect-aware package manager. |
|
| Mechtaev, Sergey |
Yihan Dai, Sijie Liang, Haotian Xu, Peichu Xie, and Sergey Mechtaev (Peking University, China; Beijing Forestry University, China; Independent, China) |
|
| Mendis, Charith |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Meng, Boning |
Chenke Liu, Li Zhou, and Boning Meng (Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) |
|
| Mezini, Mira |
Julian Haas, Ragnar Mogk, Annette Bieniusa, and Mira Mezini (Technische Universität Darmstadt, Germany; Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Germany) |
|
| Mikek, Benjamin |
Benjamin Mikek, Chathur Bommineni, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) |
|
| Mitchell, John |
Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey (Mysten Labs, USA; Stanford University, USA; Microsoft, USA; National University of Singapore, Singapore) Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date. |
|
| Møller, Anders |
Anders Møller and Işıl Dillig (Aarhus University, Denmark; University of Texas at Austin, USA) |
|
| Mogk, Ragnar |
Julian Haas, Ragnar Mogk, Annette Bieniusa, and Mira Mezini (Technische Universität Darmstadt, Germany; Rheinland-Pfälzische Technische Universität Kaiserslautern-Landau, Germany) |
|
| Müller, Peter |
Hongyi Ling, Thibault Dardinier, Ellen Arlt, and Peter Müller (ETH Zurich, Switzerland; EPFL, Switzerland; MPI-SWS, Germany) Automated program verifiers are often organized into a front-end, which encodes an input program into an intermediate verification language (IVL), and a back-end, which proves that the IVL program is correct. Soundness of such translational verifiers requires that the back-end verification is sound and that correctness of the IVL program implies correctness of the input program. Existing formalizations for translational verifiers based on separation logic target the former, but support the latter only under the strong assumption that there exists a separation logic for the input program with the same state model as the IVL. This assumption is unrealistic in practice, especially since the state model also defines the supported separation logic resources. We present the first formal framework for proving the soundness of translational separation logic verifiers with non-trivial state encodings. To be applicable to various front-ends and IVLs, our framework only assumes the existence of a homomorphic encoding relation between the front-end and IVL state models. At the core of our framework is a novel condition, backward satisfiability, which is crucial to guarantee the soundness of the front-end translation. We formalize our framework for front-end verifiers based on concurrent separation logic and separation logic IVLs, such as Raven, VeriFast, and Viper. We demonstrate its expressiveness by proving soundness for three common state encodings. Our framework and all proofs are formalized in Isabelle/HOL. Nicolas Klose and Peter Müller (ETH Zurich, Switzerland) |
|
| Murase, Yuito |
Yuito Murase and Atsushi Igarashi (Kyoto University, Japan) MetaML-style multi-stage programming (MSP) supports quasi-quotation-based code generation, runtime execution of generated code, and cross-stage persistence (CSP). However, its interaction with computational effects is subtle: mutable state can cause scope extrusion, where generated code escapes the scope of variables on which it depends. This paper presents a type system for MetaML-style MSP with mutable state that statically rules out harmful scope extrusion while supporting multi-level code generation, runtime execution, and a variant of CSP. Our system builds on refined environment classifiers (RECs), a discipline that annotates code types with the variable scopes on which generated code depends. To scale RECs to the MetaML-style setting, we refine classifiers so that they track not only variable scopes, but also the scopes of classifiers themselves. Further, we integrated polymorphism over classifiers, enabling more general and reusable code generation patterns in a multi-level setting. For the resulting system, we define an operational semantics via a definitional interpreter and prove type soundness and safety of offline code generation, showing that generated code can be extracted as standalone well-typed programs. We provide working implementations and mechanized proofs in Rocq. |
|
| Nandi, Chandrakana |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Nguyen, Dat |
Dat Nguyen, Vasudha Devarakonda, Anxiao Jiang, and Khanh Nguyen (Texas A&M University, USA) |
|
| Nguyen, Khanh |
Dat Nguyen, Vasudha Devarakonda, Anxiao Jiang, and Khanh Nguyen (Texas A&M University, USA) |
|
| Nguyen, Tien N. |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Nguyễn, Kim |
Mickaël Laurent and Kim Nguyễn (Charles University, Czech Republic; Université Paris-Saclay, France) Set-theoretic types provide a rich type algebra that supports unrestricted unions, intersections, and negations, together with a decidable type constraint-solving algorithm known as tallying. These types are particularly well suited for typing dynamic languages, where functions often exhibit both generic and overloaded behavior. However, the complexity of their implementation has hindered their widespread adoption. In this paper, we introduce a modular representation for set-theoretic types and revisit the algorithms for subtyping and tallying. We compare our approach with the historical CDuce implementation and evaluate the performance impact of some optimizations and design choices. |
|
| Ni, Haobin |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Nicolet, Victor |
Jinwoo Kim, Victor Nicolet, Joey Dodds, and Loris D'Antoni (University of California at San Diego, USA; Amazon, USA) |
|
| Niu, Xintao |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Nowacki, Todd |
Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey (Mysten Labs, USA; Stanford University, USA; Microsoft, USA; National University of Singapore, Singapore) Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date. |
|
| Odersky, Martin |
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky (EPFL, Switzerland) Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument” become inexpressible. Both arise in the Scala 3 standard library: Try re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and Future must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion (c.only[C]) and exclusion (c.except[C]). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns. Matt Bovel, Viktor Kunčak, and Martin Odersky (EPFL, Switzerland) |
|
| Omar, Cyrus |
Alexander Bandukwala and Cyrus Omar (University of Michigan, USA) |
|
| Ozga, Wojciech |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Pai, Sreepathi |
Jingyu Qiu, Rongcui Dong, and Sreepathi Pai (University of Rochester, USA) |
|
| Pal, Anjali |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Panchekha, Pavel |
Bhargav Kulkarni, Henry Whiting, and Pavel Panchekha (University of Utah, USA) Yumeng He and Pavel Panchekha (University of Utah, USA) |
|
| Pardeshi, Akash |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Parker, James |
Zhaoxiang Liu, James Parker, and Ning Luo (Kansas State University, USA; Ossa Network, USA; University of Illinois at Urbana-Champaign, USA) |
|
| Parreaux, Lionel |
Luyu Cheng, Florent Ferrari, Lionel Parreaux, and Michael D. Adams (Hong Kong University of Science and Technology, Hong Kong; ENS de Lyon, France; National University of Singapore, Singapore) Andong Fan, Lionel Parreaux, and Ningning Xie (University of Toronto, Canada; Hong Kong University of Science and Technology, Hong Kong) |
|
| Patel, Krut |
Devansh Jain, Akash Pardeshi, Marco Frigo, Kaustubh Khulbe, Krut Patel, Saatvik Lochan, Jai Arora, and Charith Mendis (University of Illinois at Urbana-Champaign, USA; NVIDIA, USA) Machine learning (ML) compilers play a key role in enabling high-performance implementations of ML workloads. These compilers use existing CPU and GPU backends to generate device-specific code. In recent years, many tensor accelerators (or AI accelerators) have been designed to further accelerate these workloads, with commercial products like AWS Trainium publicly available. However, compared to commodity hardware, a majority of tensor accelerators do not have mature ML compiler backends with robust code generation support. Moreover, tensor accelerator designs are subject to fast iteration cycles, making it difficult to manually develop and maintain ML compiler backends. Therefore, to enable faster integration of novel tensor accelerator designs in ML infrastructure, we need to make the compiler backend construction process more agile. In this paper, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. These backends are integrated with XLA, a production ML compiler. ACT uses a novel ISA-parameterized compilation algorithm to generate a compiler backend with an equality-saturation-based instruction selection phase and a constraint-programming-based memory allocation phase. We generated compiler backends for 6 accelerator platforms from industry (e.g., AWS Trainium, Intel AMX) and academia (e.g., Gemmini). We showed that these generated backends match or outperform commercial compiler backends and expert-written kernel libraries, while maintaining low compilation overheads. Notably, ACT-generated backend for AWS NKI ISA improved the code generation coverage for AWS Trainium by 2.3x compared with AWS’s production compiler, neuronx-cc. ACT is part of a larger open-source ecosystem, built around our ISA description language TAIDL, that automatically generates essential software tools, such as test oracles and compiler backends, from ISA descriptions of tensor accelerators. Our tooling has been adopted by multiple academic and industry teams designing novel tensor accelerators. The ecosystem is available at https://github.com/act-compiler/act. |
|
| Pavlogiannis, Andreas |
Amir K. Goharshady, Chun Kit Lam, Andreas Pavlogiannis, and Ahmed Khaled Zaher (Gran Sasso Science Institute, Italy; Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark) Minimizing code size is a central problem in compiler optimization, especially in the context of embedded systems and mobile applications. One of the classical optimizations that has recently been adopted to reduce the output code size is function inlining, i.e. repeatedly replacing a function call site by the body of the called function. At first glance, the fact that inlining can help reduce code size is counter-intuitive. However, it enables two types of subsequent optimizations which can affect the code size significantly: (i) the intra-procedural optimizations performed within each function, which make use of the additional context provided by inlining, and (ii) the elimination of dead functions. Many existing heuristics, such as those used by LLVM, focus on a local size analysis based on a few call sites. Thus, they miss the global opportunities to remove dead functions. On the other hand, the current state-of-the-art approach of auto-tuning by Theodoridis et al. [ASPLOS 2022] focuses on global code size but inspects each call site independently in order to avoid a combinatorial explosion. However, inlining decisions are not independent in practice. It is possible that two inlining choices each increase code size on their own, but applying both of them together reduces the size. In this work, we show that the problem of optimal inlining for code size minimization is NP-hard. We then present a completely different approach to this problem. Our algorithm is based on equality graphs (e-graphs), which are a standard tool in automated theorem proving and have recently been adopted by the compiler optimization community as a key ingredient in equality saturation. We show that optimal function inlining can be reduced to e-graph extraction. Although e-graph extraction is also NP-hard, there are efficient solvers that can handle sparse instances of this problem [OOPSLA 2024]. We build upon these solvers and add further inlining-specific heuristics to design an algorithm for code size reduction. Finally, we present experimental results on the standard SPEC benchmarks. Compared with LLVM, our approach reduces the code size to 95.34%. This is competitive with the state-of-the-art auto-tuning method of [ASPLOS 2022], which achieves 95.24%. In terms of running time, our approach is 20x faster than auto-tuning. More importantly, due to the two methods having orthogonal strengths, applying both of them leads to a further significant improvement, reducing the code size to 93.94% of LLVM's output. |
|
| Peng, Sixiang |
Sixiang Peng, Chenyang Sun, Wei Chen, Bowen Zhang, and Charles Zhang (Hong Kong University of Science and Technology, China) The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries. |
|
| Petricek, Tomas |
Tomas Petricek and Tomáš Boďa (Charles University, Czech Republic) |
|
| Pfingstl, Colin |
Daniel Galán Pascual, François Hublet, Srđan Krstić, Roman Fischer, Colin Pfingstl, and David Basin (ETH Zurich, Switzerland) Dynamic information-flow control (IFC) enforces confidentiality policies at runtime by tagging values with security labels and blocking policy-violating outputs by terminating the running system. Pervasive label tracking and enforcement checks incur high runtime costs, which limits practical IFC deployment to performance-insensitive workloads. We present a novel alternative called MinIF, a type-directed program transformation that statically eliminates the overhead of dynamic IFC for existing systems. The central contribution of MinIF is a flow-sensitive type system that tracks which sensitive inputs influence a value and whether the enforcement mechanism would accept operations on it, even though the enforced policy is unknown to the type system. Using the type system, MinIF statically predicts enforcement outcomes and removes redundant checks along with the label-tracking code that served them, and we prove that the optimized program preserves both the behavior and the enforcement decisions of the original. For IFC systems with introspection, the optimization is fully automatic, as the introspection queries already present in the program supply all the permission information MinIF needs, with no programmer annotations. Unresolved checks surface as warnings, and the absence of warnings gives developers a static guarantee against enforcement-induced system termination. We evaluate MinIF on Python programs running on the WebTTC dynamic IFC platform. On benchmarks, MinIF eliminates between 13% and 99% of the enforcement overhead, and compute-intensive workloads that time out under enforcement now complete in milliseconds. |
|
| Pham, Cao Nguyen |
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky (EPFL, Switzerland) Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument” become inexpressible. Both arise in the Scala 3 standard library: Try re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and Future must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion (c.only[C]) and exclusion (c.except[C]). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns. |
|
| Pierce, Benjamin C. |
Zain K. Aamer and Benjamin C. Pierce (University of Pennsylvania, USA) |
|
| Pinto, Elton |
Elton Pinto and Milind Chabbi (Georgia Institute of Technology, USA; Uber Technologies, USA) |
|
| Pischke, Kai |
Kai Pischke and Nobuko Yoshida (University of Oxford, UK) Multiparty session types (MPST) are a type discipline for concurrent and distributed systems, designed to ensure not only type safety and deadlock-freedom, but also liveness of typed communicating processes. Two main MPST methodologies, top-down and bottom-up, have been proposed and are integrated into a wide range of programming languages and tools. The top-down strategy starts by specifying the overall choreography of the protocol (called a global type), from which a set of local types that satisfy safety and liveness are generated by endpoint projection (EPP). Once each participant is type-checked against a generated local type, liveness of the set of typed processes is automatically ensured by construction. The bottom-up strategy directly checks whether local types inferred from processes satisfy liveness in order to enforce liveness of processes. Since the top-down strategy depends on global types and the EPP algorithms, it has often been considered that the top-down system offers strictly less typability than the bottom-up system. Our paper negates this belief. We prove that, using the precise subtyping for the subsumption rule, the top-down strategy offers exactly the same typability as the bottom-up system. More precisely, a multiparty session M is typable and verified to be live by the bottom-up typing system if and only if M is typable by the top-down typing system. The key to the proof is the development of a principal global type inference algorithm which builds a principal global type from an arbitrary set of live local types. We have implemented the global type inference algorithm together with projection, process type checking and local type inference algorithms, and built a toolchain for both the top-down and bottom-up strategies. We evaluated our toolchain with representative examples from the literature, confirming that the top-down approach is more efficient than the bottom-up approach. |
|
| Pit-Claudel, Clément |
Guokai Chen, Sergi Soler Arrufat, Clément Pit-Claudel, and Thomas Bourgeat (EPFL, Switzerland) |
|
| Pontes García, Pedro |
Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, and Adrian Sampson (Cornell University, USA) |
|
| Prokopec, Aleksandar |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Qadeer, Shaz |
Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey (Mysten Labs, USA; Stanford University, USA; Microsoft, USA; National University of Singapore, Singapore) Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date. |
|
| Qi, Yun |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Qiang, Wei |
Wei Qiang and Ronghui Gu (Columbia University, USA; Certik, New York, USA) |
|
| Qiu, Jingyu |
Jingyu Qiu, Rongcui Dong, and Sreepathi Pai (University of Rochester, USA) |
|
| Raad, Azalea |
Azalea Raad, Michalis Kokologiannakis, Viktor Vafeiadis, and Conrad Watt (Imperial College London, UK; ETH Zurich, Switzerland; MPI-SWS, Germany; Nanyang Technological University, Singapore) |
|
| Raghothaman, Mukund |
Sara Baradaran, Yifei Huang, Wei Le, and Mukund Raghothaman (University of Southern California, USA; Iowa State University, USA) |
|
| Rand, Robert |
Ben Caldwell, William Spencer, Aleks Kissinger, and Robert Rand (University of Chicago, USA; University of Oxford, UK) Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition obscures the essential connective information, leading to longer proofs filled with syntactic manipulation. To address the gap between proof assistants and paper proofs, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning over these systems. Our tactics can also be used in existing verification projects about symmetric monoidal categories that can be treated as tensors. |
|
| Regehr, John |
Siddharth Bhat, Léo Stefanesco, George Rennie, John Regehr, and Tobias Grosser (University of Cambridge, UK; University of Utah, USA) |
|
| Rennie, George |
Siddharth Bhat, Léo Stefanesco, George Rennie, John Regehr, and Tobias Grosser (University of Cambridge, UK; University of Utah, USA) |
|
| Reps, Thomas |
Benjamin Mikek, Chathur Bommineni, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) |
|
| Rompf, Tiark |
Yuyan Bao and Tiark Rompf (Augusta University, USA; Purdue University, USA) |
|
| Rong, Yi |
Yi Rong, Xupeng Li, and Ronghui Gu (Columbia University, USA; CertiK, USA) |
|
| Rosà, Andrea |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Rosenthal, Eli |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Roy, Subhajit |
Gourav Takhar, Sumit Lahiri, Pankaj Kumar Kalita, and Subhajit Roy (IIT Kanpur, India; Qualcomm, India; IBM Research, India) Modern software systems routinely invoke components whose source code is unavailable, such as proprietary libraries or cloud-based APIs. Such closed-box functions provide only oracle-style access: they can be executed on concrete inputs, but their internal logic cannot be inspected. Prior work has explored augmenting SMT solvers—the foundational engines behind contemporary automated reasoning—to handle satisfiability queries over first-order formulas containing calls to such closed-box functions. However, these approaches primarily rely on testing-based techniques to search for satisfying models and therefore do not support constructing proofs of unsatisfiability. While model search is sufficient for bug-finding tasks, the inability to generate unsatisfiability proofs fundamentally limits their applicability to formal verification. In this work, we present the first SMT solver capable of producing proofs of unsatisfiability for first-order theories that include closed-box function calls. Our key insight is to leverage large language models (LLMs) to conjecture auxiliary lemmas—based on natural language documentation of the closed-box functions—that capture properties relevant for reasoning about their behavior. To support this approach, we introduce an extension of the SMT-LIB language that allows the declaration of closed-box functions together with natural language descriptions, usage documentation, examples, and oracle interfaces. We, then, develop NLUnsat, an SMT solver that operates over this extended syntax to find unsatisfiability proofs on SMT-LIB formulas with closed-box functions. On a benchmark suite of 193 extended SMT-LIB problems involving closed-box functions, NLUnsat equipped with the openai.gpt-oss:20b LLM solves 89% of the instances, and a virtual best solver across five LLMs solves 98% of the instances. We further evaluate NLUnsat in the setting of deductive verification for programs containing closed-box function calls. On a collection of 15 benchmark programs, our verifier, using NLUnsat as its backend solver, successfully proves all verification goals when given access to a pool of two LLMs, openai.gpt-oss:20b and openai.gpt-oss:120b. Finally, we evaluate NLUnsat on satisfiable benchmark instances: none of these instances were incorrectly classified as unsatisfiable, and the solver successfully finds models for 57 out of 107 satisfiable instances. |
|
| Ryu, Sukyoung |
Seungmin Jeon, Jaeho Choi, Jonguk Jeon, Kanguk Lee, Kyeongmin Cho, Sukyoung Ryu, and Jeehoon Kang (KAIST, Republic of Korea; HyperAccel, Republic of Korea; Rebellions, Republic of Korea; FuriosaAI, Republic of Korea) Monte Carlo methods are fundamental to finance, system verification, and scientific simulation, but converge slowly: achieving an additive error of є requires O(1/є2) samples. Quantum Amplitude Estimation (QAE) offers a quadratic speedup by encoding the target probabilistic model into a quantum circuit. However, constructing such a circuit demands low-level quantum expertise, and existing tools for this task all sacrifice at least one of generality, usability, or efficiency. To address these, we design QPPL (Quantum Probabilistic Programming Language), a simple imperative language, and a compiler that translates probabilistic programs into quantum circuits. The key insight is that the circuit construction amounts to specifying a probability distribution, precisely the task that probabilistic programming addresses. QPPL achieves generality by supporting joint distributions, conditional updates, dynamic probabilities, and real-valued expectations in a single language; usability by offering a sequential, imperative syntax with named variables and direct arithmetic that hides all quantum details; and efficiency by modularly compiling each construct into reversible circuit primitives, achieving scalable circuit synthesis. We prove that the compilation is semantics-preserving. On benchmarks spanning finance and probabilistic model checking, QPPL is the only tool that covers all benchmarks, while producing circuits with up to 8.8× fewer gates and 26× shallower depth than existing tools. Jaehyun Lee, Seokhun Jeong, Sehyuk Ahn, Haechan Kwon, and Sukyoung Ryu (KAIST, Republic of Korea) Programming languages evolve over time, but often without a complete and unambiguous definition of their syntax and semantics. Ambiguities and inconsistencies are silently introduced into specifications, and manifest as divergences between the specification, implementations, and formalizations that constitute the language ecosystem. Even in rare cases when a normative specification exists, like JavaScript and WebAssembly (Wasm), keeping the ecosystem in sync is a daunting task. Language mechanization frameworks address this problem by treating a mechanized specification as the single source of truth, from which implementations and documents are generated. Recently, this approach has been integrated into the actual JavaScript and Wasm specifications with ESMeta and Wasm-SpecTec, respectively. Despite these successes, it remains an open question how to extrapolate ESMeta and Wasm-SpecTec to other language specifications. Both framework designs leverage the existence of JavaScript and Wasm’s normative specifications, which is not the case for many languages. As a first step towards addressing this question, we present P4-SpecTec, a language mechanization framework for the P4 programming language, as a case study of real-world adoption of language mechanization. P4 is a statically-typed domain-specific language for programming packet processors. It is evolving without a normative specification, thereby introducing inconsistencies and errors into the P4 ecosystem. From a mechanization framework perspective, P4 introduces unique challenges, in particular the requirement that its type system mechanization should be executable, which is not supported by either ESMeta or Wasm-SpecTec. To address this challenge, we introduce algorithmic inference rules as the primary instrument for mechanization, enabling the mechanized P4 static and dynamic semantics to be executed as a P4 type checker and interpreter, respectively. We mechanized the most recent P4 specification, and utilizing its executability, identified 24 bugs across the official P4 specification and the reference compiler. Furthermore, P4-SpecTec derives a specification document as prose algorithms, making it accessible to P4 developers. P4-SpecTec is conditionally adopted as the official P4 specification authoring toolchain. We share the lessons learned from our case study, to provide insights for integrating mechanization into real-world languages without normative specifications. |
|
| Salvaneschi, Guido |
Alexander Städing Dominguez, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi (University of St. Gallen, Switzerland) |
|
| Sampson, Adrian |
Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, and Adrian Sampson (Cornell University, USA) |
|
| Sarro, Federica |
Lyuye Zhang, He Ye, Federica Sarro, Yuqiang Sun, and Yang Liu (Nankai University, China; Nanyang Technological University, Singapore; University College London, UK) Remediating vulnerabilities in open-source software (OSS) dependencies is vital to maintaining software supply chain security. However, current automated approaches almost exclusively rely on dependency upgrades, which is limited by the nature of upgrades, i.e., the availability of secure versions, version pinning, and API incompatibilities. To address the limitation, this paper presents Remedius, an agent-based remediation framework for Maven projects that unifies dependency upgrading and patch porting within a holistic optimization workflow. Remedius dynamically clusters dependencies by usage, gathers project-specific evidence through autonomous LLM-driven agents, and formulates a cost-aware remediation optimization problem solved via Satisfiability Modulo Theory (SMT). The agents translate complex contextual factors—such as compatibility, reachability, and patch difficulty—into solver-ready constraints, enabling flexible and scalable decision-making beyond what static rules or LLM reasoning alone can achieve. By redefining optimization at the vulnerability level rather than the dependency level, Remedius maximizes vulnerability coverage while preserving build correctness and runtime compatibility. An evaluation of 301 real-world Maven projects demonstrates that Remedius outperforms state-of-the-art baselines, achieving the highest number of vulnerabilities fixed and the fewest build or test failures. These results highlight a new direction for automated OSS remediation beyond upgrade-only solutions toward adaptive, agent-driven vulnerability management. |
|
| Sergey, Ilya |
Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey (National University of Singapore, Singapore; Princeton University, USA) Relational program logics are a popular formalism for stating and proving properties that relate executions of several computations. We present Infinitary Relational Logic (IRL)—the first Hoare-style Separation Logic that allows one to state and prove relational properties of possibly infinite families of arbitrary programs. The key insights behind IRL are to (a) generalise relational program specifications in the style of Separation Logic triples to families of programs indexed by arbitrary infinite sets, and (b) provide general proof rules that support reasoning principles guided by the structure of these index sets. We have implemented IRL as a foundational embedding and verification tool on top of the Lean proof assistant. We demonstrate its power by showcasing both the practical and theoretical advances IRL brings to the state of the art in deductive program verification. To show the former, we use IRL to specify and prove the correctness of a series of previously unverified algorithms from computer graphics and geo-spatial information systems that iterate over array-encoded continuous objects. In doing so, we show that specifying representations of implicitly continuous data using code rather than traditional state invariants offers pragmatic benefits in the form of concise and reusable proofs, while retaining full compatibility with conventional non-relational Hoare-style reasoning. To show the latter, we use IRL to specify and verify a novel notion we call Weird Machine Realisability, providing the first conceptual framework that formally characterises the space of unintended behaviours permitted by a vulnerable program. All our case studies are formalised in Lean. Todd Nowacki, Sam Blackshear, John Mitchell, Shaz Qadeer, and Ilya Sergey (Mysten Labs, USA; Stanford University, USA; Microsoft, USA; National University of Singapore, Singapore) Safe systems languages such as Rust enforce an ownership discipline through types: every value has a unique owner, and the type system tracks borrows—references that provide temporary access to values without transferring their ownership. Borrow checking is a static analysis ensuring that no borrow outlives its owner and that no two mutable borrows are aliases, preventing dangling references and data races at compile time. Move, a smart contract language deployed on Sui and Aptos blockchains, adopts this model but restricts references to structured access paths rooted in local variables, eliminating the need for complex lifetime tracking mechanisms such as lifetime annotations. We present a novel type system for Move's borrow checker in which access paths are tracked by regular expressions. In this model, Brzozowski derivatives make it possible to express the reachability consequences of borrowing operations, Kleene star summarises borrow chains from function calls and loops, and the aliasing check reduces to the decidable regex emptiness. The design of the type system with regular expression-based borrow tracking extends naturally to vectors and enumeration types. The proposed design of a borrow checker has been implemented in the Move bytecode verifier for Sui blockchain, where it superseded the original borrow analyser while maintaining full backwards compatibility. We mechanised the type system in Lean with a machine-checked soundness proof and an executable algorithmic type checker tested against the production Move compiler. Notably, this 39,000-line metatheory was developed with an AI proof assistant in roughly one month, and we report on our experience of conducting this proof effort, which is among the largest AI-assisted PL metatheory mechanisations to date. Ziyi Yang and Ilya Sergey (National University of Singapore, Singapore) |
|
| Sharma, Rahul |
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India; Google DeepMind, India) |
|
| Shi, Haifeng |
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl (University of Waterloo, Canada) |
|
| Shi, Jingyi |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Shi, Yuanfeng |
Yifan Zhang, Yuanfeng Shi, Haoran Lin, Yingfei Xiong, and Xin Zhang (Peking University, China) |
|
| Shinnar, Avraham |
Lennard Gäher, Vincent Lafeychine, Sascha Kehrli, Avraham Shinnar, Wojciech Ozga, Guerney Hunt, and Derek Dreyer (MPI-SWS, Germany; Université Paris-Saclay - CNRS - ENS Paris-Saclay - Inria - LMF, France; IBM Research, USA; IBM Research Zurich, Switzerland) |
|
| Sighireanu, Mihaela |
Julien Simonnet, Matthieu Lemerre, and Mihaela Sighireanu (Université Paris-Saclay - CEA LIST, France; Université Paris-Saclay - ENS Paris-Saclay - CNRS - LMF, France) Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose relations, while assignment-based relational designs capture relations but hinder modularity and reuse. We introduce open lattices and abstract abstract datatypes (AADT), a new foundation for building precise and reusable abstract domains for structured values. Open lattices generalize classical lattices by introducing shared symbolic values constrained by an abstract valuation domain, enabling relational reasoning across independently defined abstractions. AADTs are compositional transformers over open lattices that mirror the structure of concrete data types: addresses, records, unions, variants, arrays, and their arbitrary nesting. Because each AADT closely follows the concrete datatype definition, abstract domain operations are modular and easy to reuse or extend. Most AADT transformers that we provide are exact: when the abstract valuation domain is exact, the resulting abstraction is a precise translation of the concrete semantics. This enables applications beyond static analysis, such as counter-example generation. We formalize open lattices and AADTs, present key instances, and implement them in a framework for the analysis of C and binary programs. Our experiments show precision gains over state-of-the-art abstract interpreters, while maintaining comparable analysis times. |
|
| Silva, Alexandra |
Katherine Wu, Jules Jacobs, Kevin Batz, and Alexandra Silva (Cornell University, USA; Jane Street, USA) |
|
| Simonnet, Julien |
Julien Simonnet, Matthieu Lemerre, and Mihaela Sighireanu (Université Paris-Saclay - CEA LIST, France; Université Paris-Saclay - ENS Paris-Saclay - CNRS - LMF, France) Proving properties of programs that manipulate compound data structures requires both disjunctive reasoning (e.g., a pointer may target different arrays) and relational reasoning. Existing abstract interpreters struggle to combine both: non-relational designs support modular composition of abstract domains but lose relations, while assignment-based relational designs capture relations but hinder modularity and reuse. We introduce open lattices and abstract abstract datatypes (AADT), a new foundation for building precise and reusable abstract domains for structured values. Open lattices generalize classical lattices by introducing shared symbolic values constrained by an abstract valuation domain, enabling relational reasoning across independently defined abstractions. AADTs are compositional transformers over open lattices that mirror the structure of concrete data types: addresses, records, unions, variants, arrays, and their arbitrary nesting. Because each AADT closely follows the concrete datatype definition, abstract domain operations are modular and easy to reuse or extend. Most AADT transformers that we provide are exact: when the abstract valuation domain is exact, the resulting abstraction is a precise translation of the concrete semantics. This enables applications beyond static analysis, such as counter-example generation. We formalize open lattices and AADTs, present key instances, and implement them in a framework for the analysis of C and binary programs. Our experiments show precision gains over state-of-the-art abstract interpreters, while maintaining comparable analysis times. |
|
| Singer, Jeremy |
Xiaoyang Sun, Dejice Jacob, Huanting Wang, Jeremy Singer, and Zheng Wang (University of Leeds, UK; University of Glasgow, UK) Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions. |
|
| Slaughter, Elliott |
Elliott Slaughter, Rupanshu Soi, Michael Bauer, and Alex Aiken (SLAC National Accelerator Laboratory, USA; Stanford University, USA; NVIDIA Research, USA) Checkpointing, or periodic saving of program state to storage, is the de facto standard technique used to mitigate risks of nondeterministic bugs, hardware faults, and job wall-time limits in long-running programs. Traditional approaches require users to manually manage the migration of data to and from storage when capturing checkpoints and when resuming execution. However, for task-based programs, where the user has already factored the computation into tasks and the program data into collections, sufficient information is available to automatically capture and resume from checkpoints with minimal code changes. We present Relight, the first framework for automatic, distributed checkpointing of task-based programs that provides an efficient fast-forward replay for full job recovery. On a set of already-optimized benchmarks, we demonstrate that Relight delivers checkpointing performance and scalability comparable to the original, unmodified codes when running on up to 512 nodes of the Piz Daint supercomputer. |
|
| Soi, Rupanshu |
Elliott Slaughter, Rupanshu Soi, Michael Bauer, and Alex Aiken (SLAC National Accelerator Laboratory, USA; Stanford University, USA; NVIDIA Research, USA) Checkpointing, or periodic saving of program state to storage, is the de facto standard technique used to mitigate risks of nondeterministic bugs, hardware faults, and job wall-time limits in long-running programs. Traditional approaches require users to manually manage the migration of data to and from storage when capturing checkpoints and when resuming execution. However, for task-based programs, where the user has already factored the computation into tasks and the program data into collections, sufficient information is available to automatically capture and resume from checkpoints with minimal code changes. We present Relight, the first framework for automatic, distributed checkpointing of task-based programs that provides an efficient fast-forward replay for full job recovery. On a set of already-optimized benchmarks, we demonstrate that Relight delivers checkpointing performance and scalability comparable to the original, unmodified codes when running on up to 512 nodes of the Piz Daint supercomputer. |
|
| Soler Arrufat, Sergi |
Guokai Chen, Sergi Soler Arrufat, Clément Pit-Claudel, and Thomas Bourgeat (EPFL, Switzerland) |
|
| Song, Wei |
Yichuan Li, Wei Song, Jeff Huang, and Hans-Arno Jacobsen (Nanjing University of Science and Technology, China; Texas A&M University, USA; University of Toronto, Canada) Recovering the structure of a Solidity smart contract from its deployed bytecode is a prerequisite for various downstream analyses, such as control-flow graph construction, decompilation, and clone detection. A central step in this task is identifying private functions. However, since all source-level function boundaries are completely lost after compilation, the major challenge of this task lies in how to differentiate function calls from intra-procedural control transfers, because both are implemented via the JUMP/JUMPI instructions. We observe that although jump-based control transfers are superficially uniform, their context information is different. Some contexts provide definitive evidence of an intra-procedural control transfer or a function call, which inspires us to address this problem through progressive refinement rather than naive binary classification. Specifically, we first construct an over-approximated set of potential function call sites based on EVM execution semantics, and then narrow them down using rule-based reasoning. The remaining uncertain cases are finally resolved through probabilistic inference over suggestive contexts. For each identified function, we further analyze the instructions before each jump to determine its target and reassemble scattered code fragments into a continuous instruction sequence. We implement our approach as an open-source tool, dubbed ReFun, and evaluate it on 8,696 real-world Solidity smart contracts across multiple Solidity compiler versions and optimization settings. The experimental results demonstrate that ReFun achieves 94.3% precision and 95.5% recall in function recovery, and it is also efficient, completing function identification and separation for 82% of contracts within eight seconds per contract. Finally, we show how ReFun is applied to the downstream tasks, including contract decompilation and clone detection. |
|
| Spencer, William |
Ben Caldwell, William Spencer, Aleks Kissinger, and Robert Rand (University of Chicago, USA; University of Oxford, UK) Symmetric monoidal categories (SMCs) are a common framework for reasoning about computation, focusing on the parallel and sequential compositionality of operations. String diagrams are a ubiquitous and powerful tool for reasoning about equations in SMCs, eliding the fine details of compositionality to focus on connectivity. However, when working with SMCs in a proof assistant, the rigid equational structure of composition obscures the essential connective information, leading to longer proofs filled with syntactic manipulation. To address the gap between proof assistants and paper proofs, we have developed verified tools for diagrammatic reasoning in Rocq, including inferring term equivalence and rewriting modulo the deformation of string diagrams. This is achieved by converting between syntactic representations of SMC terms and hypergraphs with interfaces, while preserving a common tensor semantics. We provide tools to develop simple SMC theories from generators and relations, and perform equational reasoning over these systems. Our tactics can also be used in existing verification projects about symmetric monoidal categories that can be treated as tensors. |
|
| Städing Dominguez, Alexander |
Alexander Städing Dominguez, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi (University of St. Gallen, Switzerland) |
|
| Stefanesco, Léo |
Siddharth Bhat, Léo Stefanesco, George Rennie, John Regehr, and Tobias Grosser (University of Cambridge, UK; University of Utah, USA) |
|
| Su, Zhendong |
Heqing Huang and Zhendong Su (City University of Hong Kong, China; ETH Zurich, Switzerland) Path coverage tracing is one of the fundamental components for supporting a wide range of dynamic program analyses, such as testing, debugging, profiling, and many others. Since one needs to insert code into a program to trace its coverage, runtime overhead becomes the main bottleneck for scalability. As finding the minimum number of instrumentation points is NP-hard, extensive work has focused on reducing the number of instrumented edges under diverse assumptions, and thus suffers from the trade-off between precision and efficiency. Departing from this edge-centric view, we introduce, in this work, a novel perspective, namely the node-centric view, where we aim to find the minimum number of blocks, rather than edges as in existing work, that can differentiate all edges and paths in the program. This new perspective allows us to design a linear-time algorithm that is provably correct and optimal—it finds the minimum set of blocks for correctly differentiating edge/path coverage for arbitrary control-flow graphs. Our key insight is that optimal node-level instrumentation only needs to distinguish undifferentiated paths at the block where they converge, enabling our algorithm to have linear-time complexity regarding the number of basic blocks. We implement our algorithm as InsOpt and compare it against state-of-the-art edge-coverage instru- mentation techniques on the real-world vulnerability-detection benchmark, Magma. Our evaluation results demonstrate significant improvements: InsOpt needs 2.8x less instrumentation with only 17% basic blocks instrumented. This reduced instrumentation yields a 1.6x speedup and a substantial 2.4x reduction in runtime overhead. Moreover, we also demonstrate substantial potential for InsOpt across other applications. Specifically, our integration of InsOpt with AFL++, a state-of-the-art fuzzer, shows a 5.0x speedup in vulnerability detection and a 1.5x performance improvement. Notably, this efficiency gain further benefits InsOpt in detecting five previously unknown bugs in frequently evaluated projects by other state-of-the-art tools. |
|
| Sun, Chenyang |
Sixiang Peng, Chenyang Sun, Wei Chen, Bowen Zhang, and Charles Zhang (Hong Kong University of Science and Technology, China) The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries. |
|
| Sun, Jiechen |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Sun, Lian |
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl (University of Waterloo, Canada) |
|
| Sun, Maolin |
Maolin Sun, Fuqi Jia, Yibiao Yang, and Yuming Zhou (Nanjing University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by integrating logical reasoning with numerical optimization to address constrained optimization problems across diverse theories. Optimizing SMT solvers (also known as OMT solvers), designed to handle such problems, serve as foundational components in numerous applications within programming languages research and practice. However, despite their widespread adoption, OMT solvers are susceptible to subtle yet critical bugs that can silently mislead downstream applications by providing incorrect optimal solutions, potentially leading to severe consequences. Validating these solvers poses a fundamental challenge, as obtaining precise ground truth for optimal solutions is inherently difficult, particularly under complex or theory-specific objective functions. Moreover, existing SMT solver testing techniques are inadequate, as they fail to capture the intricate interplay between satisfiability checking and optimization reasoning in OMT. To overcome these challenges, we propose cross-theory approximation, a novel validation methodology that leverages the relationships between solution spaces of different logical theories. The key insight is that an optimal solution produced in one theory should maintain expected relationships when interpreted in another comparable theory's solution space. By defining these cross-theory consistency properties and comparing optimal solutions obtained through theory-specific transformations, we can detect discrepancies that indicate potential solver bugs. For instance, an integer-optimal solution should map cleanly into the broader real-arithmetic domain; deviations from this expected relationship signal incorrect optimization behavior. We implement this methodology in Iris, a practical framework for validating OMT solvers. When testing on the advanced OMT solvers, including Z3 and OptiMathSAT, Iris uncovers 24 previously unknown bugs, 20 of which were subsequently resolved by developers. Notably, most of our reported bugs are correctness issues, emphasizing the effectiveness of our approach in enhancing OMT solver reliability. |
|
| Sun, Xiaoyang |
Xiaoyang Sun, Dejice Jacob, Huanting Wang, Jeremy Singer, and Zheng Wang (University of Leeds, UK; University of Glasgow, UK) Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions. |
|
| Sun, Yuqiang |
Lyuye Zhang, He Ye, Federica Sarro, Yuqiang Sun, and Yang Liu (Nankai University, China; Nanyang Technological University, Singapore; University College London, UK) Remediating vulnerabilities in open-source software (OSS) dependencies is vital to maintaining software supply chain security. However, current automated approaches almost exclusively rely on dependency upgrades, which is limited by the nature of upgrades, i.e., the availability of secure versions, version pinning, and API incompatibilities. To address the limitation, this paper presents Remedius, an agent-based remediation framework for Maven projects that unifies dependency upgrading and patch porting within a holistic optimization workflow. Remedius dynamically clusters dependencies by usage, gathers project-specific evidence through autonomous LLM-driven agents, and formulates a cost-aware remediation optimization problem solved via Satisfiability Modulo Theory (SMT). The agents translate complex contextual factors—such as compatibility, reachability, and patch difficulty—into solver-ready constraints, enabling flexible and scalable decision-making beyond what static rules or LLM reasoning alone can achieve. By redefining optimization at the vulnerability level rather than the dependency level, Remedius maximizes vulnerability coverage while preserving build correctness and runtime compatibility. An evaluation of 301 real-world Maven projects demonstrates that Remedius outperforms state-of-the-art baselines, achieving the highest number of vulnerabilities fixed and the fewest build or test failures. These results highlight a new direction for automated OSS remediation beyond upgrade-only solutions toward adaptive, agent-driven vulnerability management. |
|
| Sundram, Shiv |
Bala Vinaithirthan, Shiv Sundram, Sneha Goenka, and Fredrik Kjolstad (Stanford University, USA; Princeton University, USA) |
|
| Ta, Mier |
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl (University of Waterloo, Canada) |
|
| Takhar, Gourav |
Gourav Takhar, Sumit Lahiri, Pankaj Kumar Kalita, and Subhajit Roy (IIT Kanpur, India; Qualcomm, India; IBM Research, India) Modern software systems routinely invoke components whose source code is unavailable, such as proprietary libraries or cloud-based APIs. Such closed-box functions provide only oracle-style access: they can be executed on concrete inputs, but their internal logic cannot be inspected. Prior work has explored augmenting SMT solvers—the foundational engines behind contemporary automated reasoning—to handle satisfiability queries over first-order formulas containing calls to such closed-box functions. However, these approaches primarily rely on testing-based techniques to search for satisfying models and therefore do not support constructing proofs of unsatisfiability. While model search is sufficient for bug-finding tasks, the inability to generate unsatisfiability proofs fundamentally limits their applicability to formal verification. In this work, we present the first SMT solver capable of producing proofs of unsatisfiability for first-order theories that include closed-box function calls. Our key insight is to leverage large language models (LLMs) to conjecture auxiliary lemmas—based on natural language documentation of the closed-box functions—that capture properties relevant for reasoning about their behavior. To support this approach, we introduce an extension of the SMT-LIB language that allows the declaration of closed-box functions together with natural language descriptions, usage documentation, examples, and oracle interfaces. We, then, develop NLUnsat, an SMT solver that operates over this extended syntax to find unsatisfiability proofs on SMT-LIB formulas with closed-box functions. On a benchmark suite of 193 extended SMT-LIB problems involving closed-box functions, NLUnsat equipped with the openai.gpt-oss:20b LLM solves 89% of the instances, and a virtual best solver across five LLMs solves 98% of the instances. We further evaluate NLUnsat in the setting of deductive verification for programs containing closed-box function calls. On a collection of 15 benchmark programs, our verifier, using NLUnsat as its backend solver, successfully proves all verification goals when given access to a pool of two LLMs, openai.gpt-oss:20b and openai.gpt-oss:120b. Finally, we evaluate NLUnsat on satisfiable benchmark instances: none of these instances were incorrectly classified as unsatisfiable, and the solver successfully finds models for 57 out of 107 satisfiable instances. |
|
| Talpin, Jean-Pierre |
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen (Zhejiang University, China; Inria Rennes, France; Inria, France) |
|
| Tan, Jun |
Jun Tan and Guannan Wei (Independent, China; Tufts University, USA) |
|
| Tan, Tian |
Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li (Nanjing University, China) Heap abstraction critically affects both the efficiency and precision of pointer analysis for Java programs. By merging heap objects allocated at different program points, heap abstractions can significantly improve analysis efficiency, but often at the cost of precision. Mahjong, a state-of-the-art heap abstraction based on object merging, demonstrates that object merging can substantially improve the efficiency of pointer analysis while preserving precision for type-dependent clients; however, this client-specific guarantee limits its general applicability. In this work, we investigate how to improve the efficiency of pointer analysis through object merging, while preserving precision in a manner independent of any particular client. Our key insight is that, from the perspective of pointer analysis, many heap objects exhibit early flow confluence: they are allocated at different program points and then quickly propagate to the same pointers (variables or fields), after which they continue to flow together through the program. Merging such early-confluent objects has negligible impact on overall analysis precision. In contrast, merging objects that do not flow to the same pointers, or that converge only much later, can introduce substantial precision loss. Guided by this insight, we propose Valve, a new heap abstraction approach that efficiently identifies and merges early-confluent objects. Valve encodes the flow information needed for early-confluence detection as nondeterministic finite automata (NFAs) and approximates mergeability checking via an NFA-equivalence test, enabling efficient object merging while retaining high precision. We evaluate Valve on the largest benchmarks used in recent literature as well as modern large-scale Java applications, by integrating it with multiple state-of-the-art pointer-analysis techniques and directly comparing it with Mahjong. The results show that Valve achieves substantially higher precision than Mahjong for non-type-dependent clients, while maintaining comparable precision for type-dependent clients. At the same time, Valve delivers comparable or often better analysis efficiency across all evaluated cases. Overall, Valve, as a heap abstraction approach, significantly improves the efficiency of pointer analysis across several state-of-the-art techniques while maintaining high precision (99.61% on average). Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. |
|
| Tang, Shuyang |
Shuyang Tang, Sherman S. M. Chow, Hongfei Fu, Zihan Guo, and Guoqiang Li (Shanghai Jiao Tong University, China; Chinese University of Hong Kong, Hong Kong; Shanghai University of Finance and Economics, China; Sun Yat-sen University, China) |
|
| Tang, Yazhou |
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen (Zhejiang University, China; Inria Rennes, France; Inria, France) |
|
| Tao, Yichen |
Yichen Tao, Hongfei Fu, Jiawei Chen, and Jean-Baptiste Jeannin (University of Michigan, USA; Shanghai University of Finance and Economics, China) Floating-point round-off errors are ubiquitous in numerically intensive programs arising in fields such as scientific computing and optimization. As floating-point errors potentially lead to unexpected and catastrophic program failures, one must derive guaranteed round-off thresholds to ensure the correctness of these programs. However, deterministic round-off thresholds tend to be too conservative to be usable in practice, since they often involve large round-off errors that occur with small probability. Probabilistic thresholds relax deterministic ones by specifying that the probability of the round-off error exceeding a threshold is below a given confidence. In this work, we propose a novel approach to probabilistic round-off analysis, by applying concentration inequalities over the Taylor expansion from FPTaylor (TOPLAS 2018). A major obstacle in applying concentration inequalities is that the Taylor expansion involves absolute value operators that make the calculation of the expected values of the first order partial differential terms difficult. Our first step to overcome this obstacle is a sound over-approximation that removes the absolute value operators in polynomial expressions. Then, we show how to handle fractional expressions by a transformation into polynomial case. Finally, we show how to improve our approach with range partitioning. Our approach is scalable since the key computational part is the calculation of expected values of polynomial expressions with independent variables, for which the linear and independence properties of expectation boost the computation. Experimental results show that our approach is orders of magnitude more time efficient, while producing thresholds with comparable precision against the state of the art. |
|
| Tatlock, Zachary |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Thimmaiah, Aditya |
Aditya Thimmaiah, Tong-Nong Lin, and Milos Gligoric (University of Texas at Austin, USA) |
|
| Tjoa, Ryan |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Tsai, Wei-Lun |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| Tůma, Petr |
Jaromír Antoch, Walter Binder, Lubomír Bulej, François Farquet, Vojtěch Horký, Aleksandar Prokopec, Andrea Rosà, and Petr Tůma (Charles University, Czech Republic; USI Lugano, Switzerland; Oracle Labs, Switzerland) Recent studies of virtual machine warm up have pointed out that even small deterministic microbenchmarks executed in tightly controlled circumstances often do not reach a steady state of peak performance. This impacts performance evaluation methodologies that focus on performance after warm up, because the lack of a steady state may violate common assumptions made when computing metrics such as the average performance or the confidence interval for that average. Our work examines the reported lack of steady state in the context of comparatively larger virtual machine workloads. We document and analyze similar lack of steady state and argue that it should be considered an inherent property of these workloads rather than a fault. We introduce an updated performance evaluation methodology for workloads whose execution exhibits segments of steady state performance separated by sudden performance changes. Using the Renaissance benchmark suite for the Java Virtual Machine, we show that the methodology can produce confidence intervals that miss the true performance over 20 % less often than the existing methodologies. |
|
| Vafeiadis, Viktor |
Azalea Raad, Michalis Kokologiannakis, Viktor Vafeiadis, and Conrad Watt (Imperial College London, UK; ETH Zurich, Switzerland; MPI-SWS, Germany; Nanyang Technological University, Singapore) Ellen Arlt and Viktor Vafeiadis (MPI-SWS, Germany) |
|
| Villumsen, Jakob Schneider |
Magnus Madsen, Andreas Stenbæk Larsen, Jakob Schneider Villumsen, and Aslan Askarov (Aarhus University, Denmark) Today, most software is developed by building on packages, allowing developers to accelerate development. The proliferation of package dependencies creates a target-rich environment for malicious actors to hijack packages to inject malware, steal sensitive information, or cause destruction. Such supply chain attacks constantly threaten package ecosystems such as Cargo, npm, and Maven. In this paper, we explore how to fight against such attacks by leveraging effect systems. While effect systems predict the behavior of software components, there is a practical gap between a programming language with an effect system and a programming language ecosystem that can use such effects to thwart attacks. To close this gap, we introduce a notion of an effect-safe package upgrade and develop an effect-aware package manager that enforces safety through effect lock files. We extend the Flix programming language and its compiler toolchain with an effect-aware package manager. We evaluate the usefulness of the proposed effect-aware package manager with a case study of 51 supply chain attacks from the "Backstabbers Knife Collection" corpus of malware. The study suggests that 48 of these attacks are likely preventable with our proposed effect-aware package manager. |
|
| Vinaithirthan, Bala |
Bala Vinaithirthan, Shiv Sundram, Sneha Goenka, and Fredrik Kjolstad (Stanford University, USA; Princeton University, USA) |
|
| Vitek, Jan |
Mickaël Laurent, Pierre Donat-Bouillud, Filip Křikava, and Jan Vitek (Charles University, Czech Republic; Czech Technical University, Czech Republic) Set-theoretic types support expressive record types through unions, intersections, and negations, but they lack the row polymorphism needed to type operations that propagate unknown fields across records. Prior work addresses this by allowing Boolean combinations of rows in type substitutions, which complicates the formalism and prevents the tallying algorithm from being complete. We propose an alternative: instead of enriching substitutions, we allow Boolean combinations of row variables directly within record type constructors, where the tail of a record has the same shape as any field. This design keeps substitutions simple---a row variable maps to a single row---and yields a natural extension of the subtyping and tallying algorithms. Tallying is complete for all solutions whose rows are constant over labels not mentioned in the constraints. We implement our approach in the set-theoretic type library SSTT and the type checker MLsem, providing the first implementation of a type system that combines semantic subtyping with row polymorphism. We demonstrate the expressiveness of the system by encoding several data structures from the R programming language: heterogeneous lists, variadic function arguments, and class-based dispatch. |
|
| Vora, Keval |
Xiaoyu Liu, Qikang Liu, Evan Dyce, Keval Vora, and Yuepeng Wang (Simon Fraser University, Canada) Writing graph queries is challenging for non-experts due to the complexity of graph data models and the need to identify proper graph patterns. While recent research has advanced query synthesis for relational and document databases, the problem of synthesizing graph queries remains under-explored. We present a novel approach for synthesizing graph queries from computation demonstrations, where users specify the desired output through expressions over properties of input graphs. Our method addresses the challenge of inferring meaningful graph patterns for matching and efficiently constructing the remaining components of the query. Specifically, we combine graph mining, which identifies candidate patterns across input graphs, with deduction-based pruning, which guides an efficient synthesis of the filtering predicate and return clause. We have implemented our approach in a tool called DMiner and evaluated it on 90 benchmarks. Experimental results show that DMiner successfully synthesizes desired queries for 87 benchmarks, with an average synthesis time of 0.6 seconds per query. This outperforms both enumerative search and LLM baselines. We also conducted a user study, which shows that users can provide demonstrations with modest effort and 87.5% of the provided demonstrations are sufficient for DMiner to synthesize the desired query. |
|
| Wang, Haijun |
Xitao Li, Xiaofei Xie, Jiang Wu, Ting Liu, and Haijun Wang (Xi'an Jiaotong University, China; Singapore Management University, Singapore) |
|
| Wang, Huanting |
Xiaoyang Sun, Dejice Jacob, Huanting Wang, Jeremy Singer, and Zheng Wang (University of Leeds, UK; University of Glasgow, UK) Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions. |
|
| Wang, Jinpeng |
Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li (Nanjing University, China) Heap abstraction critically affects both the efficiency and precision of pointer analysis for Java programs. By merging heap objects allocated at different program points, heap abstractions can significantly improve analysis efficiency, but often at the cost of precision. Mahjong, a state-of-the-art heap abstraction based on object merging, demonstrates that object merging can substantially improve the efficiency of pointer analysis while preserving precision for type-dependent clients; however, this client-specific guarantee limits its general applicability. In this work, we investigate how to improve the efficiency of pointer analysis through object merging, while preserving precision in a manner independent of any particular client. Our key insight is that, from the perspective of pointer analysis, many heap objects exhibit early flow confluence: they are allocated at different program points and then quickly propagate to the same pointers (variables or fields), after which they continue to flow together through the program. Merging such early-confluent objects has negligible impact on overall analysis precision. In contrast, merging objects that do not flow to the same pointers, or that converge only much later, can introduce substantial precision loss. Guided by this insight, we propose Valve, a new heap abstraction approach that efficiently identifies and merges early-confluent objects. Valve encodes the flow information needed for early-confluence detection as nondeterministic finite automata (NFAs) and approximates mergeability checking via an NFA-equivalence test, enabling efficient object merging while retaining high precision. We evaluate Valve on the largest benchmarks used in recent literature as well as modern large-scale Java applications, by integrating it with multiple state-of-the-art pointer-analysis techniques and directly comparing it with Mahjong. The results show that Valve achieves substantially higher precision than Mahjong for non-type-dependent clients, while maintaining comparable precision for type-dependent clients. At the same time, Valve delivers comparable or often better analysis efficiency across all evaluated cases. Overall, Valve, as a heap abstraction approach, significantly improves the efficiency of pointer analysis across several state-of-the-art techniques while maintaining high precision (99.61% on average). |
|
| Wang, Ke |
Yi Zhang, Yu Wang, Ke Wang, and Linzhang Wang (Nanjing University, China) Compilers are central to software performance, yet even mature optimization pipelines such as LLVM's and GCC's often miss optimization opportunities. Existing approaches for detecting missed compiler optimizations are constrained by the challenge of reliably determining whether a specific optimization has been applied, leading to a fundamental weakness in their ability to generalize to real-world software. This paper presents a new perspective for detecting missed compiler optimizations. The key idea is utilizing compiler's native analyses to directly examine the compiler's optimized output and identify code regions that remain further optimizable---evidence that some optimization opportunities were missed. We develop two strategies to realize this idea: one that queries analyses independent of the missed optimization, effectively leveraging their otherwise unused reasoning results, and another that rewrites code into semantics-preserving forms to activate otherwise incompatible analyses. We conduct an extensive evaluation of our approach on LLVM using all 219 projects from LLVM Opt Benchmark, a suite used by LLVM developers to measure the performance impact of compiler updates on real-world software. Across these programs, our tool discovers 31,616 missed optimization opportunities. By analyzing them, we have identified and reported 25 issues to LLVM developers; 20 have already been patched or confirmed. Applying LLVM official patches to our reported issues consistently yielded runtime speedups of up to 12.96% for affected software and compile-time reductions of up to 7.55%. Hongyu Chen, Yu Wang, Jianhua Zhao, and Ke Wang (Nanjing University, China) Compiler backends are critical for translating high-level code into efficient machine instructions, yet they remain relatively underexplored in compiler testing. Effective backend testing requires programs that expose low-level backend behaviors, but such features are difficult to generate and are frequently eliminated by earlier optimization passes. As a result, existing testing approaches often fail to adequately exercise backend behaviors and are therefore less effective at uncovering backend defects. We present BackSmith, a black-box approach for testing compiler backends across compilers and architectures. BackSmith generates code snippets with two complementary properties: backend-oriented features that directly stress backend mechanisms such as instruction selection and register allocation, and optimization-resistant features that preserve program diversity by resisting excessive middle-end canonicalization. To further increase coverage of rare but critical backend behaviors, BackSmith also generates code snippets whose compiled assembly rarely arises during random generation. It then integrates all three kinds of features into seed programs for backend testing. We evaluated BackSmith on 16 mature GCC and LLVM backends. Over five months of testing, BackSmith uncovered 104 previously unknown backend bugs, 88 of which have been confirmed or fixed, demonstrating the effectiveness of our approach in systematically exposing backend defects. |
|
| Wang, Linzhang |
Yi Zhang, Yu Wang, Ke Wang, and Linzhang Wang (Nanjing University, China) Compilers are central to software performance, yet even mature optimization pipelines such as LLVM's and GCC's often miss optimization opportunities. Existing approaches for detecting missed compiler optimizations are constrained by the challenge of reliably determining whether a specific optimization has been applied, leading to a fundamental weakness in their ability to generalize to real-world software. This paper presents a new perspective for detecting missed compiler optimizations. The key idea is utilizing compiler's native analyses to directly examine the compiler's optimized output and identify code regions that remain further optimizable---evidence that some optimization opportunities were missed. We develop two strategies to realize this idea: one that queries analyses independent of the missed optimization, effectively leveraging their otherwise unused reasoning results, and another that rewrites code into semantics-preserving forms to activate otherwise incompatible analyses. We conduct an extensive evaluation of our approach on LLVM using all 219 projects from LLVM Opt Benchmark, a suite used by LLVM developers to measure the performance impact of compiler updates on real-world software. Across these programs, our tool discovers 31,616 missed optimization opportunities. By analyzing them, we have identified and reported 25 issues to LLVM developers; 20 have already been patched or confirmed. Applying LLVM official patches to our reported issues consistently yielded runtime speedups of up to 12.96% for affected software and compile-time reductions of up to 7.55%. |
|
| Wang, Sean |
Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey (National University of Singapore, Singapore; Princeton University, USA) Relational program logics are a popular formalism for stating and proving properties that relate executions of several computations. We present Infinitary Relational Logic (IRL)—the first Hoare-style Separation Logic that allows one to state and prove relational properties of possibly infinite families of arbitrary programs. The key insights behind IRL are to (a) generalise relational program specifications in the style of Separation Logic triples to families of programs indexed by arbitrary infinite sets, and (b) provide general proof rules that support reasoning principles guided by the structure of these index sets. We have implemented IRL as a foundational embedding and verification tool on top of the Lean proof assistant. We demonstrate its power by showcasing both the practical and theoretical advances IRL brings to the state of the art in deductive program verification. To show the former, we use IRL to specify and prove the correctness of a series of previously unverified algorithms from computer graphics and geo-spatial information systems that iterate over array-encoded continuous objects. In doing so, we show that specifying representations of implicitly continuous data using code rather than traditional state invariants offers pragmatic benefits in the form of concise and reusable proofs, while retaining full compatibility with conventional non-relational Hoare-style reasoning. To show the latter, we use IRL to specify and verify a novel notion we call Weird Machine Realisability, providing the first conceptual framework that formally characterises the space of unintended behaviours permitted by a vulnerable program. All our case studies are formalised in Lean. |
|
| Wang, Shaohua |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Wang, Xizao |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Wang, Yan |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Wang, Yang |
Chujun Geng, Noah Charlton, Spyros Blanas, Michael D. Bond, and Yang Wang (Ohio State University, USA) Relational data stores are widely used because they provide persistence, scalability, and fault tolerance with a simple interface. However, most data store applications configure the data store to use weak isolation for scalable performance, permitting sporadic unserializable executions that produce incorrect results or failures. Prior work uses dynamic predictive analysis to infer violations from execution traces, but existing techniques cannot handle relational (i.e., SQL) queries with complex predicates, and they predict executions that do not violate View Serializability, leading to false negatives and false positives. This paper introduces Augur, the first dynamic predictive program analysis that (1) supports data store applications with complex relational queries and (2) reports only executions that violate View Serializability. The evaluation demonstrates that Augur finds feasible, unserializable executions in OLTP-Bench programs and in the widely used e-commerce application Spree. |
|
| Wang, Yu |
Yi Zhang, Yu Wang, Ke Wang, and Linzhang Wang (Nanjing University, China) Compilers are central to software performance, yet even mature optimization pipelines such as LLVM's and GCC's often miss optimization opportunities. Existing approaches for detecting missed compiler optimizations are constrained by the challenge of reliably determining whether a specific optimization has been applied, leading to a fundamental weakness in their ability to generalize to real-world software. This paper presents a new perspective for detecting missed compiler optimizations. The key idea is utilizing compiler's native analyses to directly examine the compiler's optimized output and identify code regions that remain further optimizable---evidence that some optimization opportunities were missed. We develop two strategies to realize this idea: one that queries analyses independent of the missed optimization, effectively leveraging their otherwise unused reasoning results, and another that rewrites code into semantics-preserving forms to activate otherwise incompatible analyses. We conduct an extensive evaluation of our approach on LLVM using all 219 projects from LLVM Opt Benchmark, a suite used by LLVM developers to measure the performance impact of compiler updates on real-world software. Across these programs, our tool discovers 31,616 missed optimization opportunities. By analyzing them, we have identified and reported 25 issues to LLVM developers; 20 have already been patched or confirmed. Applying LLVM official patches to our reported issues consistently yielded runtime speedups of up to 12.96% for affected software and compile-time reductions of up to 7.55%. Hongyu Chen, Yu Wang, Jianhua Zhao, and Ke Wang (Nanjing University, China) Compiler backends are critical for translating high-level code into efficient machine instructions, yet they remain relatively underexplored in compiler testing. Effective backend testing requires programs that expose low-level backend behaviors, but such features are difficult to generate and are frequently eliminated by earlier optimization passes. As a result, existing testing approaches often fail to adequately exercise backend behaviors and are therefore less effective at uncovering backend defects. We present BackSmith, a black-box approach for testing compiler backends across compilers and architectures. BackSmith generates code snippets with two complementary properties: backend-oriented features that directly stress backend mechanisms such as instruction selection and register allocation, and optimization-resistant features that preserve program diversity by resisting excessive middle-end canonicalization. To further increase coverage of rare but critical backend behaviors, BackSmith also generates code snippets whose compiled assembly rarely arises during random generation. It then integrates all three kinds of features into seed programs for backend testing. We evaluated BackSmith on 16 mature GCC and LLVM backends. Over five months of testing, BackSmith uncovered 104 previously unknown backend bugs, 88 of which have been confirmed or fixed, demonstrating the effectiveness of our approach in systematically exposing backend defects. |
|
| Wang, Yuepeng |
Xiaoyu Liu, Qikang Liu, Evan Dyce, Keval Vora, and Yuepeng Wang (Simon Fraser University, Canada) Writing graph queries is challenging for non-experts due to the complexity of graph data models and the need to identify proper graph patterns. While recent research has advanced query synthesis for relational and document databases, the problem of synthesizing graph queries remains under-explored. We present a novel approach for synthesizing graph queries from computation demonstrations, where users specify the desired output through expressions over properties of input graphs. Our method addresses the challenge of inferring meaningful graph patterns for matching and efficiently constructing the remaining components of the query. Specifically, we combine graph mining, which identifies candidate patterns across input graphs, with deduction-based pruning, which guides an efficient synthesis of the filtering predicate and return clause. We have implemented our approach in a tool called DMiner and evaluated it on 90 benchmarks. Experimental results show that DMiner successfully synthesizes desired queries for 87 benchmarks, with an average synthesis time of 0.6 seconds per query. This outperforms both enumerative search and LLM baselines. We also conducted a user study, which shows that users can provide demonstrations with modest effort and 87.5% of the provided demonstrations are sufficient for DMiner to synthesize the desired query. |
|
| Wang, Zheng |
Xiaoyang Sun, Dejice Jacob, Huanting Wang, Jeremy Singer, and Zheng Wang (University of Leeds, UK; University of Glasgow, UK) Superoptimization is a powerful code optimization technique that generates optimized instruction sequences by exploring the space of instruction-level transformations. However, existing superoptimizers assume that pointers and integers are interchangeable, an assumption that no longer holds in memory-security-enhanced architectures like CHERI, where pointers are represented as metadata-rich capabilities with enforced bounds, permissions, and provenance. This semantic change breaks many traditional optimizations and forces CHERI compilers to adopt conservative strategies that sacrifice performance for safety. We present CapOpt, the first superoptimization framework that explicitly incorporates capability semantics into both its search space and correctness model. CapOpt introduces Provenance-Guided Stratified Synthesis (PGSS), a synthesis strategy that structures the search space around capability-aware abstractions and uses provenance-based reasoning to eliminate unsafe transformations. We also define a capability-aware equivalence model that extends conventional functional correctness to include metadata integrity. We evaluated CapOpt on an ARM-based CHERI hardware platform and the CHERI-RISC-V simulator. Experimental results show that CapOpt improves performance by up to 4.1% over the existing CHERI-LLVM toolchain, while strengthening security by tightening pointer bounds and permissions. |
|
| Watt, Conrad |
Azalea Raad, Michalis Kokologiannakis, Viktor Vafeiadis, and Conrad Watt (Imperial College London, UK; ETH Zurich, Switzerland; MPI-SWS, Germany; Nanyang Technological University, Singapore) |
|
| Wei, Anjiang |
Benjamin Driscoll, Kshitij Dubey, Anjiang Wei, Neeraj Kayal, Rahul Sharma, and Alex Aiken (Stanford University, USA; Microsoft Research, India; Google DeepMind, India) |
|
| Wei, Fang |
Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. |
|
| Wei, Guannan |
Jun Tan and Guannan Wei (Independent, China; Tufts University, USA) Dinghong Zhong, Alexander Y. Bai, Mikail Khan, and Guannan Wei (Tufts University, USA; New York University, USA; Carnegie Mellon University, USA) |
|
| Wei, Jiashen |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Weisenburger, Pascal |
Alexander Städing Dominguez, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi (University of St. Gallen, Switzerland) |
|
| Whiting, Henry |
Bhargav Kulkarni, Henry Whiting, and Pavel Panchekha (University of Utah, USA) |
|
| Wu, Jiang |
Xitao Li, Xiaofei Xie, Jiang Wu, Ting Liu, and Haijun Wang (Xi'an Jiaotong University, China; Singapore Management University, Singapore) |
|
| Wu, Katherine |
Katherine Wu, Jules Jacobs, Kevin Batz, and Alexandra Silva (Cornell University, USA; Jane Street, USA) |
|
| Wu, Rongxin |
Li Lin, Jintai Hong, Yanlin Zhuang, and Rongxin Wu (Xiamen University, China) Mutation-based fuzzing is one of the most effective techniques for uncovering bugs in Database Management Systems (DBMSs). However, its effectiveness critically depends on the quality of the initial seed queries. High-quality seeds should be syntactically and semantically valid, incorporate diverse SQL features, and encode behaviors that drive execution into bug-prone states. In practice, existing DBMS fuzzers primarily rely on SQL queries extracted from unit tests or regression suites as initial seeds, which are often limited in diversity and scale, leaving many DBMS features and execution paths unexplored. To address this limitation, we propose SmartFuzz, an automated framework for synthesizing high-quality initial SQL seeds for mutation-based DBMS fuzzing using Large Language Models (LLMs). The key insight behind SmartFuzz is that two underutilized sources---official DBMS documentation and historical crash-triggering inputs---capture complementary knowledge about DBMS feature usage and bug-relevant behaviors. SmartFuzz extracts structured features from these sources and leverages LLMs to synthesize executable, feature-rich SQL seeds that are biased toward bug-prone execution states. We integrate SmartFuzz into existing mutation-based DBMS fuzzing pipelines and evaluate it on 4 widely used DBMSs. The results demonstrate that SmartFuzz significantly improves bug discovery and code coverage compared to state-of-the-art mutation-based fuzzers. In total, SmartFuzz detects 61 previously unknown bugs, of which 60 have been confirmed and fixed by developers. |
|
| Wu, You-Jie |
Jyun-Ao Lin, Yu-Fang Chen, Jakub Havlík, Ondřej Lengál, Fang-Yi Lo, Wei-Lun Tsai, and You-Jie Wu (National Taipei University of Technology, Taiwan; Academia Sinica, Taiwan; Brno University of Technology, Czech Republic; National Taiwan University, Taiwan) Repeat-until-success (RUS) protocols implement single-qubit unitaries using measurement, classical control, and unbounded looping. Verifying their functional correctness is challenging due to the combination of probabilistic branching, unbounded looping, and the need to reason about all input states. In this paper, we develop a fully automated framework for verifying the functional correctness of these protocols. The framework is based on viewing quantum states as trees and sets of quantum states as sets of trees, which can be represented using tree automata. The particular automata model that we use are level-synchronized tree automata (), in which nondeterminism is labelled by a choice. Since we can map a sequence of choices to a particular tree (and therefore a quantum state) in the language of an LSTA, we can use the choice-sequence semantics to track input-output correspondence (which input quantum state got transformed into which output quantum state) and enable relational verification. To deal with reasoning about infinitely many quantum states, we prove a three-test theorem, which reduces verifying correctness of RUS protocols to testing correctness on finitely many inputs, enabling automatic invariant synthesis and decidable verification. We implemented our approach and identified previously unreported bugs in the RUS literature. |
|
| Xia, Xin |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Xiao, Yang |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Xie, Ningning |
Andong Fan, Lionel Parreaux, and Ningning Xie (University of Toronto, Canada; Hong Kong University of Science and Technology, Hong Kong) |
|
| Xie, Peichu |
Yihan Dai, Sijie Liang, Haotian Xu, Peichu Xie, and Sergey Mechtaev (Peking University, China; Beijing Forestry University, China; Independent, China) |
|
| Xie, Runshuo |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Xie, Xiaofei |
Xitao Li, Xiaofei Xie, Jiang Wu, Ting Liu, and Haijun Wang (Xi'an Jiaotong University, China; Singapore Management University, Singapore) |
|
| Xiong, Aosen |
Aosen Xiong, Yudi Bai, Haifeng Shi, Lian Sun, Mier Ta, and Werner Dietl (University of Waterloo, Canada) |
|
| Xiong, Yingfei |
Yifan Zhang, Yuanfeng Shi, Haoran Lin, Yingfei Xiong, and Xin Zhang (Peking University, China) |
|
| Xu, Haotian |
Yihan Dai, Sijie Liang, Haotian Xu, Peichu Xie, and Sergey Mechtaev (Peking University, China; Beijing Forestry University, China; Independent, China) |
|
| Xu, Yichen |
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky (EPFL, Switzerland) Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument” become inexpressible. Both arise in the Scala 3 standard library: Try re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and Future must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion (c.only[C]) and exclusion (c.except[C]). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns. |
|
| Xu, Zhengzi |
Jingyi Shi, Chengyue Liu, Zhengzi Xu, Yang Xiao, Xingchu Chen, Yeting Li, Wei Huo, and Yang Liu (Institute of Information Engineering at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China; Nanyang Technological University, Singapore; Imperial Global Singapore, Singapore) Locating a known source function in a stripped binary is a prerequisite for many security and software engineering tasks, including Software Composition Analysis (SCA) false-positive elimination, patch presence verification, malware analysis, code plagiarism detection, and license compliance auditing. We formalize this need as source-to-binary function localization: given the source code of a target function and its encompassing source package, determine whether the function is present in a stripped binary and, if so, report its address. Two fundamental challenges arise: cross-modal alignment, as source code and stripped binary reside in vastly different representation spaces; and similar function disambiguation, as compilation erases the symbolic features that distinguish functionally similar functions. We present XLoc, a recall-then-verify framework built on two insights. First, cross-modal alignment does not require costly and error-prone compilation; it only demands token-level alignment, a process that can be reliably approximated. Second, the information needed to disambiguate similar functions is already available on the source side and can be extracted ahead of time to guide verification. Building on these insights, XLoc implements a multi-stage recall module in which an LLM transforms source code into pseudo-decompiled representations aligned with binary decompilation output, bridging the cross-modal gap. For verification, XLoc identifies potentially confusing similar functions, extracts differential summaries, and uses them to guide the verification process toward the specific distinguishing evidence for each candidate, producing definitive accept/reject verdicts rather than similarity rankings. We evaluate XLoc on two complementary datasets spanning 196 CVEs, 480 vulnerable functions, and 756 binaries. XLoc achieves up to 84.4% localization accuracy (4.2× over the best baseline) and HM=87.1% for positive/negative discrimination (vs. 35.1% for the best baseline). These results demonstrate that XLoc can locate target functions with high accuracy, reliably discriminate between positive and negative cases, and produce definitive verdicts. |
|
| Yadavally, Aashish |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Yang, Yibiao |
Maolin Sun, Fuqi Jia, Yibiao Yang, and Yuming Zhou (Nanjing University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by integrating logical reasoning with numerical optimization to address constrained optimization problems across diverse theories. Optimizing SMT solvers (also known as OMT solvers), designed to handle such problems, serve as foundational components in numerous applications within programming languages research and practice. However, despite their widespread adoption, OMT solvers are susceptible to subtle yet critical bugs that can silently mislead downstream applications by providing incorrect optimal solutions, potentially leading to severe consequences. Validating these solvers poses a fundamental challenge, as obtaining precise ground truth for optimal solutions is inherently difficult, particularly under complex or theory-specific objective functions. Moreover, existing SMT solver testing techniques are inadequate, as they fail to capture the intricate interplay between satisfiability checking and optimization reasoning in OMT. To overcome these challenges, we propose cross-theory approximation, a novel validation methodology that leverages the relationships between solution spaces of different logical theories. The key insight is that an optimal solution produced in one theory should maintain expected relationships when interpreted in another comparable theory's solution space. By defining these cross-theory consistency properties and comparing optimal solutions obtained through theory-specific transformations, we can detect discrepancies that indicate potential solver bugs. For instance, an integer-optimal solution should map cleanly into the broader real-arithmetic domain; deviations from this expected relationship signal incorrect optimization behavior. We implement this methodology in Iris, a practical framework for validating OMT solvers. When testing on the advanced OMT solvers, including Z3 and OptiMathSAT, Iris uncovers 24 previously unknown bugs, 20 of which were subsequently resolved by developers. Notably, most of our reported bugs are correctness issues, emphasizing the effectiveness of our approach in enhancing OMT solver reliability. |
|
| Yang, Ziyi |
Ziyi Yang and Ilya Sergey (National University of Singapore, Singapore) |
|
| Yao, Xinchen |
Xinchen Yao, Wu Daiyou, and Zhiqiang Zuo (Nanjing University, China) Capturing the control-flow and/or coverage profiles of Python code becomes a pressing need for Python development community, which is commonly used in a wide spectrum of tasks including program testing/fuzzing, debugging, understanding, and optimizations. Existing tracing approaches either suffer from prohibitively high overhead or only collect approximate information, which cannot satisfy the practical requirements. In this paper, we propose to leverage modern hardware tracing modules to achieve precise and low-overhead control-flow tracing for Python programs. To this goal, we develop Pyriscope on top of CPython runtime by integrating the effective trace pruning and efficient analysis techniques. Evaluation results demonstrate the efficacy of our system. It incurs an average overhead of only 2.99% for rich-informative control-flow tracing, which is orders of magnitude smaller than that of the state of the arts. |
|
| Yao, Yuan |
Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma (Nanjing University, China; ETH Zurich, Switzerland) As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either. |
|
| Ye, He |
Lyuye Zhang, He Ye, Federica Sarro, Yuqiang Sun, and Yang Liu (Nankai University, China; Nanyang Technological University, Singapore; University College London, UK) Remediating vulnerabilities in open-source software (OSS) dependencies is vital to maintaining software supply chain security. However, current automated approaches almost exclusively rely on dependency upgrades, which is limited by the nature of upgrades, i.e., the availability of secure versions, version pinning, and API incompatibilities. To address the limitation, this paper presents Remedius, an agent-based remediation framework for Maven projects that unifies dependency upgrading and patch porting within a holistic optimization workflow. Remedius dynamically clusters dependencies by usage, gathers project-specific evidence through autonomous LLM-driven agents, and formulates a cost-aware remediation optimization problem solved via Satisfiability Modulo Theory (SMT). The agents translate complex contextual factors—such as compatibility, reachability, and patch difficulty—into solver-ready constraints, enabling flexible and scalable decision-making beyond what static rules or LLM reasoning alone can achieve. By redefining optimization at the vulnerability level rather than the dependency level, Remedius maximizes vulnerability coverage while preserving build correctness and runtime compatibility. An evaluation of 301 real-world Maven projects demonstrates that Remedius outperforms state-of-the-art baselines, achieving the highest number of vulnerabilities fixed and the fewest build or test failures. These results highlight a new direction for automated OSS remediation beyond upgrade-only solutions toward adaptive, agent-driven vulnerability management. |
|
| Yorihiro, Ayaka |
Ayaka Yorihiro, Griffin Berlstein, Pedro Pontes García, Kevin Laeufer, and Adrian Sampson (Cornell University, USA) |
|
| Yoshida, Nobuko |
Kai Pischke and Nobuko Yoshida (University of Oxford, UK) Multiparty session types (MPST) are a type discipline for concurrent and distributed systems, designed to ensure not only type safety and deadlock-freedom, but also liveness of typed communicating processes. Two main MPST methodologies, top-down and bottom-up, have been proposed and are integrated into a wide range of programming languages and tools. The top-down strategy starts by specifying the overall choreography of the protocol (called a global type), from which a set of local types that satisfy safety and liveness are generated by endpoint projection (EPP). Once each participant is type-checked against a generated local type, liveness of the set of typed processes is automatically ensured by construction. The bottom-up strategy directly checks whether local types inferred from processes satisfy liveness in order to enforce liveness of processes. Since the top-down strategy depends on global types and the EPP algorithms, it has often been considered that the top-down system offers strictly less typability than the bottom-up system. Our paper negates this belief. We prove that, using the precise subtyping for the subsumption rule, the top-down strategy offers exactly the same typability as the bottom-up system. More precisely, a multiparty session M is typable and verified to be live by the bottom-up typing system if and only if M is typable by the top-down typing system. The key to the proof is the development of a principal global type inference algorithm which builds a principal global type from an arbitrary set of live local types. We have implemented the global type inference algorithm together with projection, process type checking and local type inference algorithms, and built a toolchain for both the top-down and bottom-up strategies. We evaluated our toolchain with representative examples from the literature, confirming that the top-down approach is more efficient than the bottom-up approach. |
|
| Yuan, Shenghao |
Shenghao Yuan, Yazhou Tang, Tianci Cao, Frédéric Besson, Jean-Pierre Talpin, and Mingshuai Chen (Zhejiang University, China; Inria Rennes, France; Inria, France) |
|
| Zaher, Ahmed Khaled |
Amir K. Goharshady, Chun Kit Lam, Andreas Pavlogiannis, and Ahmed Khaled Zaher (Gran Sasso Science Institute, Italy; Hong Kong University of Science and Technology, Hong Kong; Aarhus University, Denmark) Minimizing code size is a central problem in compiler optimization, especially in the context of embedded systems and mobile applications. One of the classical optimizations that has recently been adopted to reduce the output code size is function inlining, i.e. repeatedly replacing a function call site by the body of the called function. At first glance, the fact that inlining can help reduce code size is counter-intuitive. However, it enables two types of subsequent optimizations which can affect the code size significantly: (i) the intra-procedural optimizations performed within each function, which make use of the additional context provided by inlining, and (ii) the elimination of dead functions. Many existing heuristics, such as those used by LLVM, focus on a local size analysis based on a few call sites. Thus, they miss the global opportunities to remove dead functions. On the other hand, the current state-of-the-art approach of auto-tuning by Theodoridis et al. [ASPLOS 2022] focuses on global code size but inspects each call site independently in order to avoid a combinatorial explosion. However, inlining decisions are not independent in practice. It is possible that two inlining choices each increase code size on their own, but applying both of them together reduces the size. In this work, we show that the problem of optimal inlining for code size minimization is NP-hard. We then present a completely different approach to this problem. Our algorithm is based on equality graphs (e-graphs), which are a standard tool in automated theorem proving and have recently been adopted by the compiler optimization community as a key ingredient in equality saturation. We show that optimal function inlining can be reduced to e-graph extraction. Although e-graph extraction is also NP-hard, there are efficient solvers that can handle sparse instances of this problem [OOPSLA 2024]. We build upon these solvers and add further inlining-specific heuristics to design an algorithm for code size reduction. Finally, we present experimental results on the standard SPEC benchmarks. Compared with LLVM, our approach reduces the code size to 95.34%. This is competitive with the state-of-the-art auto-tuning method of [ASPLOS 2022], which achieves 95.24%. In terms of running time, our approach is 20x faster than auto-tuning. More importantly, due to the two methods having orthogonal strengths, applying both of them leads to a further significant improvement, reducing the code size to 93.94% of LLVM's output. |
|
| Zakhour, George |
Alexander Städing Dominguez, George Zakhour, Pascal Weisenburger, and Guido Salvaneschi (University of St. Gallen, Switzerland) |
|
| Zhan, Zhongsheng |
Jinpeng Wang, Yufei Liang, Zhongsheng Zhan, Tian Tan, and Yue Li (Nanjing University, China) Heap abstraction critically affects both the efficiency and precision of pointer analysis for Java programs. By merging heap objects allocated at different program points, heap abstractions can significantly improve analysis efficiency, but often at the cost of precision. Mahjong, a state-of-the-art heap abstraction based on object merging, demonstrates that object merging can substantially improve the efficiency of pointer analysis while preserving precision for type-dependent clients; however, this client-specific guarantee limits its general applicability. In this work, we investigate how to improve the efficiency of pointer analysis through object merging, while preserving precision in a manner independent of any particular client. Our key insight is that, from the perspective of pointer analysis, many heap objects exhibit early flow confluence: they are allocated at different program points and then quickly propagate to the same pointers (variables or fields), after which they continue to flow together through the program. Merging such early-confluent objects has negligible impact on overall analysis precision. In contrast, merging objects that do not flow to the same pointers, or that converge only much later, can introduce substantial precision loss. Guided by this insight, we propose Valve, a new heap abstraction approach that efficiently identifies and merges early-confluent objects. Valve encodes the flow information needed for early-confluence detection as nondeterministic finite automata (NFAs) and approximates mergeability checking via an NFA-equivalence test, enabling efficient object merging while retaining high precision. We evaluate Valve on the largest benchmarks used in recent literature as well as modern large-scale Java applications, by integrating it with multiple state-of-the-art pointer-analysis techniques and directly comparing it with Mahjong. The results show that Valve achieves substantially higher precision than Mahjong for non-type-dependent clients, while maintaining comparable precision for type-dependent clients. At the same time, Valve delivers comparable or often better analysis efficiency across all evaluated cases. Overall, Valve, as a heap abstraction approach, significantly improves the efficiency of pointer analysis across several state-of-the-art techniques while maintaining high precision (99.61% on average). |
|
| Zhang, Bowen |
Sixiang Peng, Chenyang Sun, Wei Chen, Bowen Zhang, and Charles Zhang (Hong Kong University of Science and Technology, China) The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries. |
|
| Zhang, Charles |
Sixiang Peng, Chenyang Sun, Wei Chen, Bowen Zhang, and Charles Zhang (Hong Kong University of Science and Technology, China) The application of high-precision value-flow analysis is experiencing a paradigm shift from planned executions to online ad hoc queries driven by human auditors and AI agents. However, existing techniques struggle in this interactive setting: exhaustive offline tabulation is fundamentally intractable, while memoryless online search suffers from redundant exploration and SMT invocations. To bridge this gap, we propose SPONGE, a novel two-phase framework that accelerates ad hoc queries through boundary-anchored indexing. Offline, SPONGE employs an adaptive-depth strategy to selectively precompute feasible value-flow segments at critical procedure boundaries, optimizing SMT allocation based on traversal probability and search space complexity. Online, it utilizes an index-guided push-down search with lazy expansion to dynamically stitch these pre-verified segments, effectively bypassing redundant state exploration and pruning unsatisfiable paths. We evaluated SPONGE on 9 C/C++ projects (up to 3.8 million LoC). Results demonstrate that SPONGE drops the 95th-percentile online query time from nearly 270 s to under 50 s compared to a baseline search. Furthermore, the adaptive strategy reduces offline indexing time by 75% over a uniform approach, amortizing the offline cost in fewer than 300 queries for workloads dominated by complex queries. |
|
| Zhang, Danfeng |
Jeffrey Ching and Danfeng Zhang (Duke University, USA) |
|
| Zhang, Lyuye |
Lyuye Zhang, He Ye, Federica Sarro, Yuqiang Sun, and Yang Liu (Nankai University, China; Nanyang Technological University, Singapore; University College London, UK) Remediating vulnerabilities in open-source software (OSS) dependencies is vital to maintaining software supply chain security. However, current automated approaches almost exclusively rely on dependency upgrades, which is limited by the nature of upgrades, i.e., the availability of secure versions, version pinning, and API incompatibilities. To address the limitation, this paper presents Remedius, an agent-based remediation framework for Maven projects that unifies dependency upgrading and patch porting within a holistic optimization workflow. Remedius dynamically clusters dependencies by usage, gathers project-specific evidence through autonomous LLM-driven agents, and formulates a cost-aware remediation optimization problem solved via Satisfiability Modulo Theory (SMT). The agents translate complex contextual factors—such as compatibility, reachability, and patch difficulty—into solver-ready constraints, enabling flexible and scalable decision-making beyond what static rules or LLM reasoning alone can achieve. By redefining optimization at the vulnerability level rather than the dependency level, Remedius maximizes vulnerability coverage while preserving build correctness and runtime compatibility. An evaluation of 301 real-world Maven projects demonstrates that Remedius outperforms state-of-the-art baselines, achieving the highest number of vulnerabilities fixed and the fewest build or test failures. These results highlight a new direction for automated OSS remediation beyond upgrade-only solutions toward adaptive, agent-driven vulnerability management. |
|
| Zhang, Nairen |
Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. |
|
| Zhang, Ning |
Ning Zhang, Nongyu Di, Zenan Li, Yuan Yao, and Xiaoxing Ma (Nanjing University, China; ETH Zurich, Switzerland) As AI-generated code proliferates, formal verification—particularly through interactive theorem provers such as Rocq and Isabelle—becomes increasingly important for ensuring software correctness. However, producing machine-checked proofs in such provers remains a bottleneck. Existing solutions bring complementary strengths to proof automation: large language models (LLMs) can propose high-level proof strategies but lack local rigor; automated tactics such as CoqHammer can reliably discharge many local goals, but lack long-range planning capabilities. To combine the best of both worlds, we present Quarry, a planning-based proof synthesis framework that separates proof planning from proof execution. Specifically, Quarry asks an LLM to actively propose multiple proof decompositions with arbitrary sublemmas, type-checks them in Rocq under temporarily admitted sublemmas, and ranks candidates using a proof-state-based difficulty model estimating hammer solvability. It then recursively proves sublemmas within a bounded budget, effectively turning long proofs into sequences of hammer-solvable obligations. We implement Quarry on top of SerAPI and CoqHammer and evaluate it using multiple frontier LLMs across multiple benchmarks. The experimental results show that planning-based decomposition with solvability-aware ranking substantially improves automation while maintaining predictable cost. Under a uniform 10-minute wall-clock budget, Quarry improves over the strongest baseline by 7–13 percentage points in success rate across three Rocq benchmarks. These results demonstrate that reliable proof automation can be achieved by coordinating neural planning with symbolic execution rather than replacing either. |
|
| Zhang, Qirun |
Benjamin Mikek, Chathur Bommineni, Qirun Zhang, and Thomas Reps (Georgia Institute of Technology, USA; University of Wisconsin-Madison, USA) |
|
| Zhang, Wenmeng |
Peishan Huang, Wenmeng Zhang, Yusen Chen, and Zhenbang Chen (National University of Defense Technology, China) |
|
| Zhang, Xin |
Yifan Zhang, Yuanfeng Shi, Haoran Lin, Yingfei Xiong, and Xin Zhang (Peking University, China) |
|
| Zhang, Yi |
Yi Zhang, Yu Wang, Ke Wang, and Linzhang Wang (Nanjing University, China) Compilers are central to software performance, yet even mature optimization pipelines such as LLVM's and GCC's often miss optimization opportunities. Existing approaches for detecting missed compiler optimizations are constrained by the challenge of reliably determining whether a specific optimization has been applied, leading to a fundamental weakness in their ability to generalize to real-world software. This paper presents a new perspective for detecting missed compiler optimizations. The key idea is utilizing compiler's native analyses to directly examine the compiler's optimized output and identify code regions that remain further optimizable---evidence that some optimization opportunities were missed. We develop two strategies to realize this idea: one that queries analyses independent of the missed optimization, effectively leveraging their otherwise unused reasoning results, and another that rewrites code into semantics-preserving forms to activate otherwise incompatible analyses. We conduct an extensive evaluation of our approach on LLVM using all 219 projects from LLVM Opt Benchmark, a suite used by LLVM developers to measure the performance impact of compiler updates on real-world software. Across these programs, our tool discovers 31,616 missed optimization opportunities. By analyzing them, we have identified and reported 25 issues to LLVM developers; 20 have already been patched or confirmed. Applying LLVM official patches to our reported issues consistently yielded runtime speedups of up to 12.96% for affected software and compile-time reductions of up to 7.55%. |
|
| Zhang, Yifan |
Yifan Zhang, Yuanfeng Shi, Haoran Lin, Yingfei Xiong, and Xin Zhang (Peking University, China) |
|
| Zhang, Yihong |
Oliver Flatt, Anjali Pal, Yihong Zhang, Ryan Tjoa, Kirsten Graham, Alex Fischman, Chandrakana Nandi, Eli Rosenthal, Zachary Tatlock, and Haobin Ni (University of Washington, USA; Certora, USA; Google, USA) |
|
| Zhang, Yiyu |
Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
|
| Zhao, Jianhua |
Hongyu Chen, Yu Wang, Jianhua Zhao, and Ke Wang (Nanjing University, China) Compiler backends are critical for translating high-level code into efficient machine instructions, yet they remain relatively underexplored in compiler testing. Effective backend testing requires programs that expose low-level backend behaviors, but such features are difficult to generate and are frequently eliminated by earlier optimization passes. As a result, existing testing approaches often fail to adequately exercise backend behaviors and are therefore less effective at uncovering backend defects. We present BackSmith, a black-box approach for testing compiler backends across compilers and architectures. BackSmith generates code snippets with two complementary properties: backend-oriented features that directly stress backend mechanisms such as instruction selection and register allocation, and optimization-resistant features that preserve program diversity by resisting excessive middle-end canonicalization. To further increase coverage of rare but critical backend behaviors, BackSmith also generates code snippets whose compiled assembly rarely arises during random generation. It then integrates all three kinds of features into seed programs for backend testing. We evaluated BackSmith on 16 mature GCC and LLVM backends. Over five months of testing, BackSmith uncovered 104 previously unknown backend bugs, 88 of which have been confirmed or fixed, demonstrating the effectiveness of our approach in systematically exposing backend defects. |
|
| Zhao, Qiyuan |
Vladimir Gladshtein, Qiyuan Zhao, Yuxi Ling, Sean Wang, and Ilya Sergey (National University of Singapore, Singapore; Princeton University, USA) Relational program logics are a popular formalism for stating and proving properties that relate executions of several computations. We present Infinitary Relational Logic (IRL)—the first Hoare-style Separation Logic that allows one to state and prove relational properties of possibly infinite families of arbitrary programs. The key insights behind IRL are to (a) generalise relational program specifications in the style of Separation Logic triples to families of programs indexed by arbitrary infinite sets, and (b) provide general proof rules that support reasoning principles guided by the structure of these index sets. We have implemented IRL as a foundational embedding and verification tool on top of the Lean proof assistant. We demonstrate its power by showcasing both the practical and theoretical advances IRL brings to the state of the art in deductive program verification. To show the former, we use IRL to specify and prove the correctness of a series of previously unverified algorithms from computer graphics and geo-spatial information systems that iterate over array-encoded continuous objects. In doing so, we show that specifying representations of implicitly continuous data using code rather than traditional state invariants offers pragmatic benefits in the form of concise and reusable proofs, while retaining full compatibility with conventional non-relational Hoare-style reasoning. To show the latter, we use IRL to specify and verify a novel notion we call Weird Machine Realisability, providing the first conceptual framework that formally characterises the space of unintended behaviours permitted by a vulnerable program. All our case studies are formalised in Lean. |
|
| Zhao, Yaoyu |
Cao Nguyen Pham, Oliver Bračevac, Yichen Xu, Yaoyu Zhao, and Martin Odersky (EPFL, Switzerland) Capture checking in Scala 3 enables lightweight and practical effect and resource tracking by recording capabilities in types. However, the system offers no way to reason about kinds of capabilities. Natural constraints such as “retaining only the control-flow capabilities of this closure” or “excluding all thread-local capabilities from this argument” become inexpressible. Both arise in the Scala 3 standard library: Try re-throws caught exceptions, so it retains only the control-flow capabilities of its body, and Future must not capture thread-local resources. The inability to state these constraints has kept parts of the library outside capture checking. We introduce capability classifiers: a tree-structured, user-extensible hierarchy of tags that classify capabilities by their semantic role. Projections filter capture sets by classifier, supporting both inclusion (c.only[C]) and exclusion (c.except[C]). The tree structure enables decidable disjointness reasoning: classifiers on separate branches are guaranteed to be disjoint regardless of unknown extensions elsewhere in the hierarchy. We formalize classifiers as an extension of System Capless, a core calculus for capture checking, introducing a classifier kind algebra based on intersection, union, and subtraction of classifier subtrees. We extend the operational semantics to model exception interception and establish type safety, effect safety, and handler coverage via a big-step proof, fully mechanized in Lean 4. Classifiers are implemented in the Scala 3 capture checker, and we demonstrate their use on standard library types and real-world effect exclusion patterns. |
|
| Zheng, Yanan |
Yan Wang, Ling Ding, Jiechen Sun, Tien N. Nguyen, Shaohua Wang, Aashish Yadavally, Xin Xia, and Yanan Zheng (Central University of Finance and Economics, China; Independent, China; University of Texas at Dallas, USA; University of Central Florida, USA; Zhejiang University, China; Yale University, USA) Large language models (LLMs) have shown strong performance in static code tasks like code search, summarization, and generation, but remain limited in dynamic code reasoning, which involves inferring how programs behave during execution without actually running them. This limitation stems from LLMs being trained on static code and lacking the necessary runtime context. In this paper, we present T-REX, a novel teacher-student framework for execution prediction that addresses these limitations by grounding LLM training in actual execution and corresponding execution semantics. T-REX uses a large teacher model (Explainer) to generate fine-grained, stepwise natural language rationales explaining how program state transitions from one statement to another during actual execution. These rationales are used to train a smaller student model (Reasoner) to predict next program states, enabling accurate simulation of program behavior with lower computational cost. Our execution-grounded, rationale-driven training aligns with transition-aware execution semantics at the statement level, enhancing prediction accuracy. Our experiments show that T-REX enables Reasoner to outperform much larger GPT-4o and GPT-4o-mini models across multiple dimensions of runtime behavior prediction, while also aiding in static detection of runtime errors as well as in debugging. Finally, we discuss how T-REX can be generalized to static emulation of any dynamic analysis through such a teacher-student distillation, illustrating with the specific case of dynamic program slicing in Python. |
|
| Zhong, Dinghong |
Dinghong Zhong, Alexander Y. Bai, Mikail Khan, and Guannan Wei (Tufts University, USA; New York University, USA; Carnegie Mellon University, USA) |
|
| Zhou, Li |
Chenke Liu, Li Zhou, and Boning Meng (Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) |
|
| Zhou, Yuming |
Maolin Sun, Fuqi Jia, Yibiao Yang, and Yuming Zhou (Nanjing University, China; Institute of Software at Chinese Academy of Sciences, China; University of Chinese Academy of Sciences, China) Optimization Modulo Theories (OMT) extends Satisfiability Modulo Theories (SMT) by integrating logical reasoning with numerical optimization to address constrained optimization problems across diverse theories. Optimizing SMT solvers (also known as OMT solvers), designed to handle such problems, serve as foundational components in numerous applications within programming languages research and practice. However, despite their widespread adoption, OMT solvers are susceptible to subtle yet critical bugs that can silently mislead downstream applications by providing incorrect optimal solutions, potentially leading to severe consequences. Validating these solvers poses a fundamental challenge, as obtaining precise ground truth for optimal solutions is inherently difficult, particularly under complex or theory-specific objective functions. Moreover, existing SMT solver testing techniques are inadequate, as they fail to capture the intricate interplay between satisfiability checking and optimization reasoning in OMT. To overcome these challenges, we propose cross-theory approximation, a novel validation methodology that leverages the relationships between solution spaces of different logical theories. The key insight is that an optimal solution produced in one theory should maintain expected relationships when interpreted in another comparable theory's solution space. By defining these cross-theory consistency properties and comparing optimal solutions obtained through theory-specific transformations, we can detect discrepancies that indicate potential solver bugs. For instance, an integer-optimal solution should map cleanly into the broader real-arithmetic domain; deviations from this expected relationship signal incorrect optimization behavior. We implement this methodology in Iris, a practical framework for validating OMT solvers. When testing on the advanced OMT solvers, including Z3 and OptiMathSAT, Iris uncovers 24 previously unknown bugs, 20 of which were subsequently resolved by developers. Notably, most of our reported bugs are correctness issues, emphasizing the effectiveness of our approach in enhancing OMT solver reliability. |
|
| Zhuang, Yanlin |
Li Lin, Jintai Hong, Yanlin Zhuang, and Rongxin Wu (Xiamen University, China) Mutation-based fuzzing is one of the most effective techniques for uncovering bugs in Database Management Systems (DBMSs). However, its effectiveness critically depends on the quality of the initial seed queries. High-quality seeds should be syntactically and semantically valid, incorporate diverse SQL features, and encode behaviors that drive execution into bug-prone states. In practice, existing DBMS fuzzers primarily rely on SQL queries extracted from unit tests or regression suites as initial seeds, which are often limited in diversity and scale, leaving many DBMS features and execution paths unexplored. To address this limitation, we propose SmartFuzz, an automated framework for synthesizing high-quality initial SQL seeds for mutation-based DBMS fuzzing using Large Language Models (LLMs). The key insight behind SmartFuzz is that two underutilized sources---official DBMS documentation and historical crash-triggering inputs---capture complementary knowledge about DBMS feature usage and bug-relevant behaviors. SmartFuzz extracts structured features from these sources and leverages LLMs to synthesize executable, feature-rich SQL seeds that are biased toward bug-prone execution states. We integrate SmartFuzz into existing mutation-based DBMS fuzzing pipelines and evaluate it on 4 widely used DBMSs. The results demonstrate that SmartFuzz significantly improves bug discovery and code coverage compared to state-of-the-art mutation-based fuzzers. In total, SmartFuzz detects 61 previously unknown bugs, of which 60 have been confirmed and fixed by developers. |
|
| Ziegler, Parker |
Parker Ziegler, David Minh-Duy Cao, Justin Lubin, and Sarah E. Chasins (University of California at Berkeley, USA) |
|
| Zuo, Zhiqiang |
Xinchen Yao, Wu Daiyou, and Zhiqiang Zuo (Nanjing University, China) Capturing the control-flow and/or coverage profiles of Python code becomes a pressing need for Python development community, which is commonly used in a wide spectrum of tasks including program testing/fuzzing, debugging, understanding, and optimizations. Existing tracing approaches either suffer from prohibitively high overhead or only collect approximate information, which cannot satisfy the practical requirements. In this paper, we propose to leverage modern hardware tracing modules to achieve precise and low-overhead control-flow tracing for Python programs. To this goal, we develop Pyriscope on top of CPython runtime by integrating the effective trace pruning and efficient analysis techniques. Evaluation results demonstrate the efficacy of our system. It incurs an average overhead of only 2.99% for rich-informative control-flow tracing, which is orders of magnitude smaller than that of the state of the arts. Fang Wei, Qinlin Chen, Nairen Zhang, Jiacai Cui, Tian Tan, Zhiqiang Zuo, and Yue Li (Nanjing University, China) Set-based (a.k.a. bit-vector-based) dataflow analysis is a fundamental building block for many static analysis tasks, and significant effort has been devoted to accelerating it. Existing acceleration approaches address the problem from a software perspective, leveraging various general-purpose computing platforms, such as single- and multi-core CPUs, GPUs, and distributed systems. In contrast, a hardware-centric approach—designing specialized hardware that directly accelerates dataflow analysis—remains unexplored. Motivated by this gap and out of pure research curiosity, we conduct a preliminary exploration of designing specialized hardware for dataflow analysis using FPGAs, which are highly customizable and well suited for rapidly prototyping domain-specific hardware. As a first step toward hardware-accelerated dataflow analysis, we focus on the widely used intra-procedural dataflow analysis. However, we find that designing specialized hardware even for this setting is already challenging: a straightforward FPGA implementation of the classical worklist algorithm is infeasible, because its space complexity grows superlinearly with procedure size, quickly exhausting the FPGA's limited high-speed on-chip memory when analyzing large procedures. To address this challenge, we introduce FpgaFlow, a specialized hardware design for dataflow analysis that (1) overcomes the spatial infeasibility challenge by leveraging the distributivity of set-based dataflow analysis to achieve linear spatial scalability, and (2) accelerates analysis through hardware-specific parallelism—pipelining with data forwarding and BRAM partitioning and replication. We evaluate FpgaFlow on diverse and popular real-world Java projects (averaging 32.5k GitHub stars) using two representative dataflow analyses—live variables and reaching definitions—and compare it against their software implementations in a state-of-the-art Java static analyzer Tai-e. In terms of correctness, FpgaFlow produces exactly the same analysis results as Tai-e, amounting to 75 billion bits. In terms of acceleration, even on a modest Xilinx Zynq-7020 FPGA (55 MHz), FpgaFlow achieves an average speedup of 15.45x for live variables and 12.32x for reaching definitions compared with Tai-e running on a server-grade CPU (2.20 GHz to 3.00 GHz). We hope this work offers useful insights toward future FPGA-accelerated static analysis. Jiashen Wei, Baoyuan Luo, Runshuo Xie, Yun Qi, Yiyu Zhang, Xizao Wang, Xintao Niu, and Zhiqiang Zuo (Nanjing University, China) Datalog has become a widely adopted language in program analysis, security, and data-intensive systems. However, debugging Datalog programs remains fundamentally challenging due to their declarative semantics, lack of explicit control flow, and massive scale of derived facts. Existing approaches, such as inspecting proof trees, algorithmic debugging, or interactive debugging, all require developers to manually navigate through deeply recursive derivations, which quickly becomes infeasible for real-world programs. In this paper, we take a step toward fully automated debugging of Datalog programs. Our key insight is to reinterpret Datalog execution through a statistical lens: instead of explaining individual facts, we analyze multiple facts collectively, treating derived facts as test cases and their proof trees as execution spectra. This abstraction enables us to adapt Spectrum-based Fault Localization (SBFL) to Datalog, bridging the paradigm gap between declarative logic programs and automated debugging techniques originally designed for imperative languages. To enable systematic evaluation, we construct, to the best of our knowledge, the first benchmark suite for Datalog debugging, comprising 96 real-world instances (37 unique faults) mined from the evolution history of the Doop framework. Each instance is annotated with ground-truth faulty rules and organized under a three-level fault taxonomy. Experimental results demonstrate that our approach effectively localizes faults without any user interaction. The best suspiciousness metric achieves 87.50% Hit@1 (i.e., top-1 hit rate) for faulty rule localization, while faulty predicate localization reaches 37.50%–53.12% Hit@1. |
391 authors
proc time: 4.09