Modern compilers are frequently updated, but expert review capacity is highly limited, leading to delayed integration and, in some cases, subtle semantic bugs entering the compiler codebase. Automating the code review process with modern general code review agents may be feasible, but it faces critical challenges due to compiler complexity. In this paper, we use LLVM as our target compiler and present Archer, the first automated agentic code review tool for compiler optimizations. Archer constrains the agentic review process from both ends by using obligations to guide analysis and a deterministic validation guard to admit only findings backed by executable evidence.

We evaluated Archer on 70 open PRs and 328 closed PRs in LLVM from the last two months. The review results are shocking and concerning: Archer discovers that 21% of open PRs and 11% of closed PRs are buggy, i.e, introducing semantic bugs such as miscompilations in LLVM. Our findings expose a critical gap in the capacity for critical review in large compiler projects and demonstrate the practical value of Archer as an additional reviewer.

Compiler missed optimizations refer to cases in which compilers failed to optimize certain code. It takes many compiler developers’ efforts to implement or patch such missed optimizations. In this paper, we present a systematic study of how well agents patch compiler missed optimizations. We identify a significant challenge that patching a missed optimization requires more than just fixing the reported case, and instead requires generalizing to similar cases. We construct a benchmark of real-world LLVM missed optimization issues and compare agent-generated patches with patches from developers in terms of optimization scope. Our results show that coding agents often optimize the given examples, but many generated patches either cover only part of the developer-intended scope or partially overlap with it; in some cases, they further generalize beyond the reference patch. We further introduce historical-knowledge augmentation techniques that leverage prior LLVM optimization pull requests through retrieval and distillation, showing that they improve developer-aligned generalization and yield practical benefits when applied to real-world IR.

CodeQL is the de facto static analysis framework integrated into GitHub and is widely used to develop custom vulnerability-detection rules. However, its compilation pipeline is difficult to inspect, modify, or extend, limiting experimentation with new language features, custom predicates, and external reasoning engines.

In this paper, we present Qoufflé, an extensible QL compiler that translates QL—CodeQL’s object-oriented logic programming language—into Datalog programs executed by the open-source Soufflé engine. Qoufflé provides an extensible compilation path for QL by resolving modern CodeQL libraries, constructing a typed IR, lowering QL-specific constructs to Soufflé, and supporting non-relational operations through external functors. We describe how Qoufflé handles key production QL features beyond prior Core QL formalizations, including parameterized modules, built-in predicates, higher-order predicates, recursive universal quantifiers, and standard and monotonic aggregation, while realizing ADT tuple-numbering semantics in Soufflé. We evaluate Qoufflé on 650 official QL test cases, where it produces results identical to CodeQL, and on 132 runs over real-world DaCapo applications. We also demonstrate its extensibility through a case study that combines QL-derived relations with external declarative reasoning.

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, yet such features are difficult to generate and are often eliminated by earlier optimization passes. As a result, existing testing approaches frequently fail to exercise diverse backend behaviors and therefore miss deep crashes and miscompilations.

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 exhibits unique patterns. 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 deep backend defects.

Code transpilation—translating code between programming languages while preserving semantics—is essential for software modernization. While large language models (LLMs) have become promising transpilers, their black-box nature and probabilistic generation often introduce subtle semantic errors, making semantic correctness difficult to verify, which limits their practical reliability. To address this, we propose a refutation framework that focuses on detecting localized semantic errors rather than verifying complete correctness. By modeling the transpilation around code fragments, our framework introduces a structured and localized analysis approach to the otherwise opaque behavior of model-based code transpilers. With this framework, we selectively identify localized semantic errors, allowing us to bypass the need for global reasoning while retaining effectiveness. We validate the framework through transpilations involving Java, Python, and C++. We first formalize their shared semantics and incorporate language-specific features, then use our refutation framework to detect unpreserved semantics. We implement this approach in a tool named RefuTra, evaluated on about 7400 real-world transpilation tasks. RefuTra can detect and repair semantic errors across multiple language pairs. Results provide preliminary evidence that our framework is a practical and effective approach to improving semantic safety in code transpilation, with potential applicability to real-world code.

在有限精度的计算中，数学上正确的浮点表达式也可能产生误差。Herbie 通过生成候选表达式，并在与高精度参考值采样对比后选择误差较低的结果来改进表达式。然而，Herbie 只能从已经生成的候选中选择结果，如果某种稳定形式没有进入候选集合，后续评估也无法利用它。大语言模型（LLM）有可能给出 Herbie 搜索不到的数值稳定重写，但直接把 LLM 输出当作最终优化结果并不可靠：多次调用可能得到不同结果，部分重写会使误差升高，而且仍需独立的数值验证。

本文提出一种 LLM 引导的模板蒸馏方法，将经过验证的 LLM 重写转化为 Herbie 可复用的数值模板。该方法在同一组采样点和高精度参考值下比较原始表达式、Herbie 输出和 LLM 输出；找出 Herbie 误差高而 LLM 误差较低的重写，再将其变换前/后结构蒸馏为可复用的模板，并把这些模板作为候选生成模块接入 Herbie。最终表达式仍由 Herbie 现有的度量、剪枝和选择流程决定。在 25 个 LLM 相对 Herbie 显著降低误差的源表达式中，23 个被成功蒸馏为模板。在 290 个高误差表达式上，该方法相较于 Herbie 产生了 34 个误差更低的结果，将优化后平均误差从 4.727 bits 降至 3.284 bits，最大单表达式误差降低 58.693 bits，且未观察到回退。在 25 个 Herbie 优化后高误差的外部验证表达式上，我们的方法改进了 15 个表达式。结果说明，经过验证的 LLM 重写可以被整理为确定性的、可复用的且可泛化的浮点优化知识。

Floating-point computations are important for modern scientific and engineering software, especially for safety-critical systems, yet only a small subset of inputs typically trigger substantial numerical errors. Detecting such error-inducing inputs and the underlying bugs is therefore essential for improving their security and reliability. Existing techniques commonly rely on either oracle-driven exploration that repeatedly compares against high-precision references or search-driven heuristics. Despite the improvements made, they remain limited by (1) Expensive computation of high-precision oracles and (2) Lack of long-range convergence, which often requires dense probing near narrow error-inducing regions and expensive computation.

We propose MGDE (Mathematically-Guided Detection of floating-point Errors), a method that replaces trial-and-error exploration with mathematically defined targets and directed convergence. MGDE first uses condition-number theory to identify numerically unstable atomic operations without invoking expensive high-precision oracles during exploration. MDGE exploits the observation that extreme condition numbers occur near structured boundaries (e.g., cancellation points and singularities), reformulating detection as a numerical root-finding problem. By solving the resulting objectives with the Newton-Raphson method, MGDE can steer inputs toward error-prone regions from far-away initializations.

We evaluate MGDE on GNU Scientific Library (GSL) functions and compare against two state-of-the-art baselines, ATOMU and FPCC, using triggered bugs as the primary metric. On 88 single-input functions, MGDE triggers 80 bugs across 47 functions, outperforming ATOMU (70 bugs in 46 functions) and FPCC (53 bugs in 42 functions). MGDE is also faster: ATOMU and FPCC require 41.71X and 10.17X more time, respectively. Regarding multi-input functions, we evaluate MGDE under two complementary settings. On the native multi-input dataset of FPCC, MGDE detects 28 triggered bugs, while FPCC finds 23 bugs. MGDE also takes 8.91 seconds in total, compared with 2,100 seconds used by FPCC. On an additional external benchmark of 18 dual-input GSL functions, MGDE detects nine bugs not found by FPCC. Overall, MGDE substantially advances the state-of-the-art in both effectiveness and efficiency, and we report 16 previously unknown GSL bugs, which have been confirmed by the GSL community.

Mutexes are fundamental synchronization primitives in concurrent programming, but their improper use can lead to deadlocks. Conventional assume-based modeling abstracts mutex semantics via assumptions, simplifying safety verification but hindering deadlock verification. Although prior efforts have aimed to address this limitation, we show that state-of-the-art methods remain inaccurate. In this paper, we propose a novel modeling approach that captures mutex semantics using ordering constraints, enabling accurate deadlock verification within partial-order-based concurrent verification frameworks. We formally prove the correctness of our method and implement it in a prototype tool, Deagle-DL. We evaluate Deagle-DL against a state-of-the-art bounded model checker ESBMC that employs the conventional modeling approach, and a state-of-the-art static analysis tool for deadlock detection. Our experiments show that Deagle-DL significantly outperforms both tools in terms of precision, while maintaining substantial efficiency.

Distributed concurrency bugs occur when concurrent execution flows, at least one of which is triggered by inter-node communication such as remote procedure calls (RPCs), access the same shared variable or object in conflicting ways, causing incorrect behavior under certain interleavings. Existing work for detecting distributed concurrency bugs focuses on dynamic approaches, thus suffering from limited coverage. This paper proposes Themis, a novel approach that uses static analysis to detect potential races, applies LLM-based test generation, and employs directed fuzzing to refine input parameters for detecting distributed concurrency bugs. We have implemented a prototype of Themis and evaluated it on eight real-world distributed systems. Themis detects 198 new violations corresponding to 52 new bugs.

Bash script comprehension is a significant challenge in Linux environments due to Bash’s syntactic freedom and complex command structures. Despite its critical role in system administration and development, Bash scripts often lack adequate comments, hindering code readability and maintainability. Existing approaches to automated Bash comment generation face two main challenges: (1) Limited training datasets that inadequately represent real-world Bash usage patterns, particularly for complex multi-line scripts; and (2) Insufficient understanding of Bash-specific concepts by Large Language Models (LLMs). Our empirical analysis shows that even after standard training, LLMs still struggle to precisely understand complex Bash command semantics, leading to inaccurate comments. To address these challenges, we propose Bash-Commenter, an advanced comment generation method based on LLaMA-3.1-8B. First, to overcome data limitations (Challenge 1), we construct a comprehensive dataset of complex, multi-line Bash scripts with high-quality comments. Second, to enhance semantic understanding (Challenge 2), we conduct Continual Pre-training (CPT) on large-scale Bash script data, followed by Supervised Fine-tuning (SFT) on our annotated dataset, strengthening the model’s foundational knowledge of Bash syntax and semantics. Finally, to resolve the subtle semantic errors that persist, we introduce Syntax-Aware Preference Optimization (SAPO). This method automatically constructs preference pairs by applying single, atomic operations (e.g., modifying a command option or removing an argument) to a script’s Abstract Syntax Tree (AST), creating minimal pairs of correct and subtly incorrect scripts. This final optimization stage enables fine-grained command semantics learning and context-dependent quality assessment, significantly improving comment accuracy. We evaluate Bash-Commenter on single-line Bash commands and multi-line Bash scripts. Our method outperforms state-of-the-art baselines, achieving 33.40% BLEU-4, 58.26% METEOR, and 57.03% ROUGE-L for 1,064 single-line commands, and 22.15% BLEU-4, 43.89% METEOR, and 32.80% ROUGE-L for 1,046 multi-line scripts. Moreover, human evaluation and LLM evaluation demonstrate the superior quality of comments generated by Bash-Commenter in terms of correctness, completeness, and naturalness.

本文介绍 QCP 在复杂 C 程序功能正确性验证中的设计思路，以及它如何为 AI 辅助验证提供工具基础。QCP 以分离逻辑符号执行为核心，结合可定制断言变换、SMT 求解、Rocq 证明后端和 IDE 增量反馈，在表达能力和自动化程度之间取得平衡。在此基础上，本文讨论让 AI 通过工具调用参与验证工程的方式：AI 代理生成候选规约、标注和证明脚本，QCP 与 Rocq 负责符号执行、验证条件生成和证明检查。围绕这一管线，本文概述谓词设计、函数准备、规约编写、标注填充和 VC 证明五个环节，并介绍我们在智能体设计和若干典型算法程序自动验证上的实践。

Program reduction simplifies bug-triggering programs while preserving a target property. It is especially important in compiler testing and debugging, where automatically generated programs are often large and hard to analyze. Most existing reducers work at the source level, using syntactic or structure-preserving transformations to shrink programs. However, preserving a target property often depends not only on source structure but also on runtime behavior, creating a gap between source-level reduction and identifying the minimal code needed to preserve the property.

In this paper, we introduce execution-guided program reduction, a new reduction perspective that focuses on the execution behavior required for preserving the target property. Our key idea is that, for many reduction tasks, especially those involving runtime properties, what matters is the execution sequence that preserves ψ. Based on this insight, we model program execution as a sequence of program states and transitions, construct a reduction sequence from the executions relevant to ψ, and adopt a ddmin-based procedure to minimize it. For each candidate reduction sequence, we construct candidate execution sets by collapsing removed transition segments into synthesized state-restoration transitions, reconstruct candidate source programs from these executions, and validate them against ψ.

We implement this approach for C programs in a tool called Exe-Reduce, which represents executions using execution traces and memory snapshots, integrated with C-Reduce, a widely-used source-level reducer. Our evaluation on both a widely used benchmark suite and real-world GCC bug reports shows that Exe-Reduce achieves substantially smaller execution sizes while maintaining competitive token-count reduction.

The theory of Equality with Uninterpreted Functions (EUF) is fundamental to constraint solving and program verification. Uninterpreted functions abstract concrete implementations, enabling generalization and simplification of theorems and proofs. However, standard EUF restricts function composition to fixed finite depths (\emph{e.g.}, $f^k(x)$ where $k$ is constant). This work extends EUF to EUF$^n$, supporting \emph{parametric composition depth} for unary functions (\emph{e.g.}, $f^n(x)$ where $n$ is a natural number variable).

An EUF$^n$ formula can be viewed as a disjunction of infinitely many EUF formulas, each instantiated by an assignment of natural numbers. Its satisfiability is defined by the satisfiability of at least one such instantiated EUF formula. We establish the decidability of the EUF$^n$ satisfiability problem via a \emph{conditional congruence graph (CCG)} algorithm. This approach generalizes the standard congruence closure procedure by maintaining conditional equivalence relations between terms. The algorithm reduces the satisfiability problem to deciding existential sentences in Presburger arithmetic with divisibility, which is a decidable problem, thereby yielding a decision procedure for the quantifier-free fragment of EUF$^n$ with a 2NEXPTIME complexity upper bound.

The enhanced expressiveness of EUF$^n$ enables new applications: (1) Encoding a decidable subclass of interleaved Dyck reachability problems where existing over/under-approximations produce false positives/negatives, and (2) Encoding a new decidable subclass of uninterpreted program verification problems.

(This paper has been accepted to OOPSLA 2026 Round 2.)

Hybrid testing that integrates fuzzing, symbolic execution, and sampling has demonstrated superior testing efficiency compared to individual techniques. However, the state-of-the-art (SOTA) hybrid testing tools do not fully exploit the capabilities of symbolic execution and sampling in two key aspects. First, the SOTA hybrid testing tools employ tailored symbolic execution engines that tend to over-prune branches, leading to considerable time wasted waiting for seeds from the fuzzer and missing opportunities to discover crashes. Second, existing methods do not apply sampling to the appropriate branches and therefore cannot utilize the full capability of sampling. To address these two limitations, we propose a novel hybrid testing architecture that combines the precision of conventional symbolic execution with the scalability of tailored symbolic execution engines. Based on this architecture, we propose several principles for combining fuzzing, symbolic execution, and sampling. %Additionally, we develop an advanced search strategy as part of the coordination mechanism.} We implement our method in a hybrid testing tool \method. To evaluate its effectiveness, we conduct extensive experiments on 15 real-world programs. Experimental results demonstrate that \method\ outperforms the SOTA tool, achieving an average improvement of 6.14% in edge coverage and 32.6% in discovered crashes. Notably, our tool uncovers three previously unknown crashes in real-world programs.

本文研究布尔（AND–OR）半环上的精确张量分解与最小线网电路构造。针对高维离散搜索中连续松 弛易发生梯度饥饿、直接 SMT 求解又遭遇组合爆炸的问题，提出“低维 SMT 精确综合–克罗内克 确定性扩展–逻辑综合验证”框架：先由 Z3 搜索并验证低维稀疏分解基块，再利用张量的克罗内克 自相似性将其零误差扩展至高维，最后通过 ABC 的 strash、resyn2 与组合等价性检查验证所得电 路。该方法将难以处理的全局优化转化为可认证的局部综合与无需再训练的代数扩展。

面向航空航天控制软件，特别是可重复使用火箭回收飞控中自然语言需求难以可靠转换为控制代码的问题，本文提出一种以中文状态转移矩阵（State Transition Matrix，STM）为核心的可解释可信建模与验证方法。航天控制软件包含飞行阶段切换、工作模式管理、故障处置、机构联锁和时间约束等复杂业务逻辑，其需求通常以自然语言编写，容易产生术语理解偏差、条件遗漏、量词和阈值二义、时间语义弱化以及异常分支不完整等问题。大模型能够提高需求结构化和代码生成效率，但其概率生成和幻觉问题可能导致虚构模型元素、修改需求参数或遗漏关键约束，因此生成结果不能直接作为安全关键控制代码的可信依据。本文采用LoRA微调的Qwen3-Coder-32B生成需求结构候选，并将状态、事件、守卫条件、时间约束、动作和目标状态映射为中文STM。由于STM中的模型元素继续采用与原始需求一致的中文业务语义，并与需求条款建立对应关系，工程人员能够逐项审查自然语言到模型的转换过程，从而实现语义可解释。在此基础上，通过结构一致性检查、状态机路径分析、测试用例生成、ZIPC动态仿真和Simulink联合仿真验证STM行为，将未经验证的大模型候选结果转化为具有测试和仿真证据的可信模型。通过验证的同一STM进一步用于C代码生成，减少模型到实现阶段的再次人工解释，形成需求—STM—测试—仿真—代码的可解释/可信链路。本文以可重复使用火箭回收触地确认为例，对至少三条支腿载荷、垂直速度阈值、50 ms连续保持及条件失效复位等复合需求进行验证。结果表明，该方法能够将大模型生成结果置于可审查、可测试和可追溯的工程流程中，为提高航空航天控制软件需求验证能力及需求—代码一致性提供一种可行方法。

Interactive Bayesian program analysis enhances static analysis by modeling derivations as probabilistic dependencies, enabling ranking alarms by calculated confidences, proposing highly likely alarms for user inspection, and updating confidences with inspection results. Existing interactive approaches adopt a purely greedy, exploitation-only selection strategy that always inspects the highest-confidence alarm. However, such strategies are prone to local optima, leading to redundant inspections and delayed identification of true alarms. We propose BEER (Bayesian Exploration–Exploitation Ranker), a framework that systematically integrates the exploration–exploitation trade-off into Bayesian program analysis. BEER leverages structural correlations between alarms—derived from shared root causes in the Bayesian model—to estimate information gain and guide exploration. When repeated false alarms indicate model stagnation, BEER selects alarms from minimally explored, highly correlated clusters to accelerate learning. Implemented atop the Bingo framework, BEER achieves up to 38% effectiveness in ranking efficiency over the greedy baseline on data-race and thread-escape analyses, demonstrating the efficacy of exploration-guided alarm resolution.

Correctly rounded elementary functions must return the oracle-rounded result for every target-format input and rounding mode. RLIBM-family generators provide this strong contract, but their linear-programming-based coefficient search can be expensive and may leave large residual exact-case sets.

This paper presents \tool{}, a checker-in-the-loop generator that replaces the LP coefficient search with centered Taylor search on the range-reduced residual domain. \tool{} searches over Taylor degree, expansion center, segment count, floating-point evaluation order, and bounded exact-case branches. It emits ordinary C and accepts a candidate only after checking the complete generated function, including special cases, range reduction, table lookup, polynomial evaluation, reconstruction, and rounding-mode behavior.

On the 12 single-precision RLIBM-MR benchmark functions, \tool{} passes all 48 full-domain function–rounding-mode checks. Its recorded generation stages are \textbf{26.0}$\times$ lower than RLIBM-MR’s interval-plus-polynomial stages, exact-case coverage drops from 46,543 to 119 binary32 inputs, and the generated code runs \textbf{1.063–1.074}$\times$ faster on average across two hosts.

The correctness of modern effectful programs depends not only on their final results but also on the temporal evolution of observable interactions with their environments. Interaction Trees (ITrees) provide a reusable denotational semantics for such programs by representing effectful computations as potentially infinite trees of observable interactions. However, reusable temporal reasoning over ITrees remains largely unexplored. This paper presents a compositional temporal specification framework for ITrees. We introduce iBuchi, a shallowly embedded temporal specification language based on Choice Trees, which represents finite and infinite interaction traces and supports expressive temporal operators, including sequencing, branching, conjunction, repetition, and Linear Temporal Logic modalities. We define trace- and tree-level satisfaction relations between iBuchi specifications and ITrees, together with compositional reasoning principles for modular verification of effectful programs. We integrate iBuchi into the Dijkstra Monads Forever framework, thereby enabling temporal specifications to compose with conventional Hoare-style specifications and supporting a generator-based encoding of future conditions. We have formally developed and verified our framework in Rocq and demonstrated its expressiveness and compositionality through several non-trivial case studies.

A recently proposed Live Verification framework promises real-time feedback during program-proof co-development of C programs in the Rocq theorem prover. However, it supports only a simplified subset of C, limiting its applicability to realistic C programs. We present C*, a verifier that shifts the prover-centric approach to a program-centric one: users write implementations, specifications, and in-situ proof code in C, while a proof-supporting verifytime separates program-logic reasoning from assertion-logic reasoning. C* supports a substantial subset of C and is extensible via user-defined proof libraries and trusted automation procedures. We evaluate C* on standard benchmarks and conduct a case study towards verifying a sequential version of pKVM’s hyp_allocator, demonstrating that live verification scales to realistic C code.

Rust has emerged as a prominent systems programming language that uniquely combines high performance with strong memory-safety guarantees, making it particularly suitable for safety-critical domains such as operating systems and blockchain technologies. However, ensuring the correctness of Rust programs remains a significant challenge, primarily due to its complex language features—including the ownership model, lifetimes, and the complicated borrow checking mechanisms. Formal verification provides a rigorous methodology to address these challenges. Tools such as Verus and Kani have been developed for this purpose and have been successfully applied to verify real-world Rust systems. This talk introduces Trust2 (website: https://trust2proj.github.io/), an open project aimed at building a formally verified toolchain for Rust using Isabelle/Rocq. The toolchain is designed to incorporate formal semantics, program verifiers, static analyzers, verified compilers, and certified code generators for Rust. Trust2 is structured into three layers: -Semantic Foundation: Mechanizing the semantics of Rust and its intermediate representations, e.g., Mid-level Intermediate Representation (MIR), in Isabelle/HOL, forming a basis for formal reasoning about Rust programs; -Verified Toolchain: Developing Rust-focused verification tools leveraging existing backends (e.g., Isabelle/HOL and Z3) and formal techniques such as separation logic, abstract interpretation, and symbolic execution; -Industrial Applications: Applying the verified toolchain to real-world systems written in Rust, including operating systems, virtual machines, compilers, and blockchain platforms.

Formal verification helps ensure software correctness and reliability. Rust is gaining popularity as a safer alternative to C due to its strong memory safety guarantees. As a result, many projects seek to migrate C code to Rust. However, the migration of C programs annotated with formal specifications remains unexplored. This paper investigates the feasibility of migrating C code annotated with ACSL specifications to verifiable Rust with Verus specifications. We present C2VR (C to Verifiable Rust), a semi-automated framework that migrates both C code and ACSL specifications. When applied to 175 annotated C programs, the framework automatically produces 92 formally verified Rust programs, and achieves 139 verified programs with manual fixes, demonstrating its effectiveness. We then conduct an empirical evaluation to assess the soundness and benefits of specification migration within our framework. The results show that our specification migration is semantics-preserving and that Verus reduces the burden of memory-related specifications, although two patterns of ACSL specifications remain non-migratable. We further classify migration failures into three major categories with a total of 15 symptoms, systematically identify 10 root causes, and present 9 effective repair strategies.

Rust 基于所有权与借用机制的类型系统能够保障内存安全，却无法保证程序具有良好的性能表现或合理的资源消耗。基于自动摊还资源分析（Automatic Amortized Resource Analysis，AARA）的 RaRust 分析器通过对共享借用和可变借用中的势能进行建模，实现了对 safe Rust 程序的自动资源分析。然而，RaRust难以直接分析 unsafe Rust程序的资源开销。这是因为 unsafe Rust 允许执行 safe Rust 所禁止的底层操作，这些危险操作可能破坏 RaRust 所依赖的安全借用模型及其别名假设。为放宽所有权规则对程序的限制，unsafe Rust 被广泛用于标准库、底层数据结构以及外部函数接口（FFI）的实现。这类代码通常将 unsafe 操作封装在内部，并向外提供 safe API，从而在维持安全接口的同时扩展 Rust 的表达能力。为了刻画此类 safe API 对其 unsafe 实现的资源抽象，我们需要一个能够同时描述借用与别名行为、资源所有权及资源消耗的语义基础。 然而，现有工作尚不足以实现这一目标：以 RustBelt 为代表的语义类型系统主要为 unsafe 代码提供内存安全和封装安全的语义模型，并不关心别名模型；而 Stacked Borrows 等别名模型主要刻画底层指针操作与别名行为，没有为 unsafe 代码提供 safe API 的语义类型。为此，我们建立一个基于分离逻辑（separation logic）的资源感知语义类型（semantic typing）模型，通过对类型进行逻辑解释，刻画 safe API 所封装的借用、别名与资源行为，并为其提供资源语义保障。 本文提出了 ResBor，一个资源感知的借用演算以及基于分离逻辑的语义类型系统。ResBor 采用 Stacked Borrows 的简化版本作为别名模型，定义了资源感知的操作语义。我们使用 Iris 框架为 ResBor 定义了资源感知的程序逻辑、资源感知类型的逻辑解释、以及类型系统的语义类型规则。ResBor 的可靠性定理在该框架下得到了形式化的陈述与证明，确保良类型程序的资源消耗不超过类型标注的上界。据我们所知，这是首次在分离逻辑中为资源感知的借用机制建立语义类型系统。目前该可靠性证明正在 Rocq/Iris 中进行形式化验证。

We present our ongoing work on verifying a Rust compiler frontend in Rocq and connecting it with CompCert to build an end-to-end verified Rust compiler, which we call RustCompCert. Its overall structure consists of three components: (1) an unverified parser that translates source Rust code into Rustlight, a sequential subset of Rust formalized in Rocq; (2) a verified frontend that compiles Rustlight to Clight, including Rust-specific passes such as Drop Elaboration and Borrow Checking; and (3) a verified backend based on CompCert, an optimizing compiler that compiles Clight to assembly. For this, we use the framework of CompCertO, an extension of CompCert, to support verified compositional compilation.

Static analysis has profoundly improved software quality over the past decades, evolving from compiler-integrated optimizations and simple linting to sophisticated analyses for bug detection, security, and program understanding. In contrast, static analysis for hardware remains underexploited, resembling the early state of software analysis. Most existing hardware static analyses are confined to compiler optimizations and linting, lacking the sophistication needed to uncover complex design flaws. Furthermore, we observe that many hardware bugs reported in recent literature could have been identified by sophisticated static analyses that account for hardware-specific semantics and data flow; however, such bug detection analyses are absent today. To exploit the untapped potential of sophisticated hardware analysis, we present a series of bug detection analyses for Verilog, the predominant hardware description language (HDL). Moreover, these analyses are built upon our fundamental analyses that capture essential hardware-specific characteristics—such as bit-vector arithmetic, register synchronization, and digital component concurrency—and enable the examination of hardware data and control flows. Together, these analyses form a well-organized analysis suite with a modular design, in which diverse fundamental analyses combine to support bug detection, hardware understanding, and other potential clients. To implement these analyses, we further offer dedicated infrastructure, including a Verilog front end, an intermediate representation (IR) for analysis, and an analysis manager. To validate the utility of our analyses, we applied them to real-world hardware projects. Unlike software, real-world hardware projects tend to contain fewer but harder-to-detect bugs, as they typically undergo extensive simulation and rigorous verification to prevent the prohibitive costs of hardware defects. Despite this, our preliminary experimental results are highly promising: applying these proposed analyses to popular real-world Verilog projects (averaging 1.5K+ GitHub stars) uncovered nine previously unknown bugs, all confirmed by developers; moreover, we successfully identified a total of 18 bugs beyond the capabilities of existing static analyses for Verilog bug detection (i.e., linters). These results underscore the transformative potential of sophisticated static analysis in hardware design. Our analysis suite and infrastructure are also highly reusable: on average, each bug-detection client built on our analysis suite requires about 270 LoC, compared to 5,700 LoC when developed from scratch. By open-sourcing the entire system, involving substantial engineering effort (100K+ LoC), we aim to encourage further innovation and applications of sophisticated static analysis for hardware, hopefully fostering a similarly vibrant ecosystem that software analysis enjoys.

General frameworks such as FlowDroid, IccTA, P/Taint, Amandroid, and DroidSafe have significantly advanced the development of static analysis tools for Android security by providing fundamental facilities for them. However, while these frameworks have been instrumental in fostering progress, they often operate with inherent inefficiencies, such as redundant computations, reliance on separate tools, and unnecessary complexity, which are rarely scrutinized by the analysis tools that depend on them. This paper introduces PacDroid, a new static analysis framework for detecting security vulnerabilities in Android apps. PacDroid employs a simple yet effective pointer-analysis-centric approach that naturally manages alias information, interprocedural value propagation, and all Android features it supports (including ICC, lifecycles, and miscs), in a unified manner. Our extensive evaluation reveals that PacDroid not only outperforms state-of-the-art frameworks in achieving a superior trade-off between soundness and precision (F-measure) but also surpasses them in both analysis speed and robustness; moreover, PacDroid successfully identifies 77 real security vulnerability flows across 23 real-world Android apps that were missed by all other frameworks. With its ease of extension and provision of essential facilities, PacDroid is expected to serve as a foundational framework for various future analysis applications for Android.

Second-order vulnerabilities, such as second-order Cross-Site Scripting (XSS) and Server-Side Request Forgery (SSRF), occur when user-controlled inputs are stored in databases and later retrieved in different execution contexts, complicating static detection. Existing static analysis approaches struggle primarily with two challenges. First, they struggle in accurately identifying database-accessing functions defined by third-party libraries or custom data access layers, often leading to missed taint propagation paths. Second, they may fail to contextually model database operations when queries are dynamically constructed and depend on runtime parameters. To address these limitations, we propose STaint, a novel bi-directional static analysis method that integrates taint analysis with large language models (LLMs). Using semantic reasoning, STaint accurately identifies and models custom database reads and writes, effectively reconstructing comprehensive taint data flows in the database. Preliminary evaluations on ten real-world PHP applications show that STaint successfully detects 56 second-order vulnerability paths, including 7 previously unknown cases, outperforming existing techniques.

Constraint solving remains a fundamental challenge in symbolic execution. To reduce the computational overhead of SMT solvers, modern symbolic execution tools commonly cache and reuse the results of previously solved queries. However, existing caching mechanisms primarily focus on satisfiable queries, offering limited support for unsatisfiable ones, which are still delegated to the underlying SMT solver. To address this problem, we introduce a novel Unsatisfiable Core Guided (Ucg) constraint solving framework for symbolic execution. The proposed framework accelerates constraint solving by systematically exploiting unsatisfiable cores, which provide compact explanations for unsatisfiability. Specifically, Ucg first constructs an unsatisfiable core cache with a least-recently-used (LRU) replacement policy to enable the reuse of previously computed unsatisfiable cores. Upon a cache miss, Ucg further exploits the temporal locality of assertions within unsatisfiable cores to predict a potential unsatisfiable core for the pending query. This predicted core serves as an over-approximation of the original query and is likely to be unsatisfiable. By solving this much smaller over-approximated formula, Ucg can infer the satisfiability of the original query with substantially reduced SMT solver effort. We integrated Ucg into Klee, a state-of-the-art symbolic execution tool for C programs. Experimental results on 99 open-source real-world programs demonstrate that Ucg consistently improves the efficiency of both constraint solving and path exploration in symbolic execution across various search strategies. In the best-case scenario, Ucg can achieve improvements of up to two orders of magnitude.

Context sensitivity improves the precision of interprocedural dataflow analysis, but coarse-grained selection performs redundant work when only a few statements benefit. Existing techniques generally select whole methods or use domain-specific selection units. We present statement-level context sensitivity, which assigns each statement either a sensitive or an insensitive policy. The main challenge is that interleaving statements with different policies can create both context-specific and shared information for the same analysis component; naively copying shared information into every context erodes the expected efficiency gains. We therefore introduce a compression-based semantics that stores and propagates shared information through a distinguished shared context. For monotonic dataflow analyses whose producers satisfy a componentwise expansion condition, we prove that the compressed and uncompressed semantics are observationally equivalent. This condition is weaker than IFDS/IDE distributivity, enabling a broader class of analyses. We evaluate the framework on a numerical analysis and a real-world pointer analysis. In the numerical analysis, statement-level selection achieves a 1.61x speedup over method-level selection while preserving the same query results For pointer analysis, lifting a state-of-the-art selector to statement-level choices yields 1.06x and 1.08x speedups under 2- and 3-object sensitivity, respectively, with identical query results and no additional domain-specific selection rules. These results show that statement-level context sensitivity can improve existing selectors across distinct dataflow analyses.

Abstract semantics has proven to be instrumental for accelerating search-based program synthesis, by enabling the sound pruning of a set of incorrect programs (without enumerating them). One may expect \emph{faster} synthesis with increasingly \emph{finer-grained} abstract semantics. Unfortunately, to the best of our knowledge, this is not the case, yet. The reason is because, as abstraction granularity increases—while fewer programs are enumerated—pruning becomes more costly. This imposes a fundamental limit on the overall synthesis performance, which we aim to address in this work.

Our key idea is to introduce an \emph{offline presynthesis} phase, which consists of two steps. Given a DSL with abstract semantics, the first \emph{semantics modeling} step constructs a tree automaton $\mathcal{A}$ for \emph{a space of inputs}—such that, for any program $P$ and for any considered input $I$, $\mathcal{A}$ has a run that corresponds to $P$’s execution on $I$ under abstract semantics. Then, the second step builds an oracle $\mathcal{O}$ for $\mathcal{A}$. This $\mathcal{O}$ enables fast pruning \emph{during synthesis}, by allowing us to efficiently find exactly those DSL programs that satisfy a given input-output example under abstract semantics.

We have implemented this \emph{presynthesis-based synthesis paradigm} in a framework, \textsc{Foresighter}. On top of it, we have developed three instantiations for SQL, string transformation, and matrix manipulation. All of them significantly outperform prior work in the respective domains.

In modern software development, Python third-party libraries play a critical role, especially in fields like deep learning and scientific computing. However, API parameters in these libraries often change during evolution, leading to compatibility issues for client applications reliant on specific versions. Python’s flexible parameter-passing mechanism further complicates this, as different passing methods can result in different API compatibility. Currently, no tool can automatically detect and repair Python API parameter compatibility issues. To fill this gap, we introduce PCART, the first solution to fully automate the process of API extraction, code instrumentation, API mapping establishment, compatibility assessment, repair, and validation. PCART handles various types of Python API parameter compatibility issues, including parameter addition, removal, renaming, reordering, and the conversion of positional to keyword parameters. To evaluate PCART, we construct PCBench, a large-scale benchmark comprising 47,478 test cases mutated from 844 parameter-changed APIs across 33 popular Python libraries. Evaluation results demonstrate that PCART is both effective and efficient, significantly outperforming existing tools (MLCatchUp and Relancer) and the large language model ChatGPT (GPT-4o), achieving an F1-score of 96.51% in detecting API parameter compatibility issues and a repair precision of 91.97%. Further evaluation on 30 real-world Python projects from GitHub confirms PCART’s practicality. We believe PCART can significantly reduce the time programmers spend maintaining Python API updates and advance the automation of Python API compatibility issue repair.

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.

Python dominates AI development and is the most widely used dynamic programming language, but synthesizing its polymorphic functions into hardware remains challenging. Existing HLS solutions support only static subsets of Python, forcing CPU offload with costly communication overhead. We present Pyls, the first framework that synthesizes dynamically polymorphic Python into monolithic hardware via Left-Child Right-Sibling (LCRS) encoding. Key to our approach is representing all Python objects as LCRS trees, enabling uniform hardware handling of dynamic types. PYLS automatically converts objects to fixed-width formats, generates XLS IR designs, and implements a tree memory architecture for efficient runtime type resolution. On FPGA platforms, PYLS demonstrates speedups of 5.19× and 3.98× over two ASIC CPUs, 303.29× over a soft-core processor, and 282.66× over a heterogeneous SoC design.

With the proliferation of open Instruction Set Architectures (ISAs) like RISC-V, achieving rapid yet reliable hardware implementation has become a paramount challenge. Traditional Hardware Description Languages (HDLs) such as Verilog suffer from weak typing, often masking bit-width mismatches and boundary errors. Meanwhile, modern agile HDLs like Chisel postpone critical safety checks until generation or simulation. To bridge this gap, we present Pella, a novel hardware description infrastructure embedded in the Coq proof assistant. The core innovation of Pella is the use of Dependent Types to encode hardware bit-width and indexing constraints directly into type signatures. Built upon a customized vector foundation, Pella enforces strict bit-width alignment across all arithmetic and structural operations at the type level. We validate Pella by constructing two RISC-V RV32I processor models—a single-cycle core and a Wildcat-style 3-stage pipeline with data forwarding— both extracted to executable OCaml code and verified through comprehensive simulation. A 92-test benchmark suite covering instruction compliance, algorithm execution, and cross-verification between the two models achieves a 100% pass rate.

Multi-stage programming with quotations has long provided a powerful way to generate and manipulate code. By treating code as data, programmers can write multi-stage programs in which earlier stages produce specialized code from inputs available at generation time. Modern typed multi-stage languages (e.g., MetaML, MetaOCaml, Template Haskell, and Scala 3) adopt quotation/splicing constructs while enforcing the well-typedness of generated code. However, manipulating code fragments syntactically can subtly change evaluation order, leading to semantic discrepancies between a staged program and its unstaged counterpart, which is intended to serve as a reference implementation in many cases. The inconsistency complicates reasoning about correctness, and prevents staged code from being a drop-in replacement for its unstaged counterpart.

In this paper, we study the design of multi-stage languages with semantics preservation guarantees. We develop two statically typed two-stage calculi, lang and langref, the latter supporting mutable references in the second stage. Their dynamic semantics models automatic let-insertion, tracked as a control effect in a lightweight type-and-effect system, enabling type-safe and semantics-preserving manipulation of effectful code fragments. We develop binary logical relations to prove strong semantics-preservation theorems: if a well-typed two-stage program t1 evaluates to a value code t2, then t2 is contextually equivalent to the stage-erasure of t1. Our calculi and their mechanized metatheory provide a simple and definitive answer to the question posed by Inoue and Taha of when staging annotations preserve semantics, and lay a foundation for future work on semantics-preserving multi-stage programming.

Note: The paper has been accepted at OOPSLA 2026 Round 2 and will appear in the ACM Proceedings of the ACM on Programming Languages this year.

递归类型用于描述自引用数据结构及返回自身类型的对象接口，在编程语言中应用广泛。然而，如何组合独立开发的递归组件，依然是类型系统设计中的一大难题。本报告将以模块化程序设计中的经典挑战——“表达式问题（Expression Problem）”为切入点，重新审视这一难题。

同构递归子类型（iso-recursive subtyping）为解决该问题提供了部分思路。本报告将首先回顾一系列我们旨在构建可复用元理论的研究工作，涵盖声明式规约、高效的算法化形式、其与等递归类型（equi-recursive types）的关系，以及向不同类型系统的扩展。在此基础上，我们进一步指出：借助交类型（intersection types）和合并算子（merge operator），递归组件的组合问题可以转化为一条尚待补全的子类型规则——即交类型对递归类型的分配律（distributivity）。最后，我们将介绍如何算法化该规则的最新进展。当前方案将递归分配律限制在“弱正类型比较”（weakly positive comparisons）范围内，并将传统的一元检查（unary check）推广为基于集合的多元极性检查（set-based polarity tracking）。我们相信，该元理论能为实用类型系统及编程语言中递归组件的扩展与组合奠定坚实基础。

Collaborative editing systems allow users to update shared data concurrently, work offline, and eventually converge once updates are exchanged. Secure replicated data types (SRDTs) extend this model to role-aware collaboration by projecting shared data into role-specific replicated views. However, SRDTs are specialized to simple tree structures and path-based projection views. This makes it difficult to support common data structures such as arrays, as well as views that go beyond fixed paths, such as value-dependent selection, where a view includes elements satisfying a predicate, and recursive extraction. This paper presents a framework for collaborative editing over role-specific views without restricting shared data to simple trees or views to fixed projections. Our key idea is to introduce lenses into CRDT-based collaborative editing as a general mechanism for specifying and synchronizing editable role-specific views with the shared source data. To integrate lenses with CRDTs, the framework introduces a lens source-lifting algorithm and coordinates source and view updates using a lens-based concurrent synchronization protocol. We implement the framework in VIEWSYNC, a prototype for collaborative editing over JSON role-specific views, and demonstrate its feasibility and expressiveness through two applications.

Bash scripts are the cornerstone of system administration and DevOps automation, where code quality directly impacts system stability and security. In automated Bash script generation using Large Language Models (LLMs), two interconnected failures emerge: unauditable “black box” reasoning and critical robustness vulnerabilities in generated code. To address both, we propose BashCoder-R1, a novel framework for robust and explainable Bash script generation. Our pipeline combines: (1) Continual Pre-training (CPT) to specialize the model on Bash paradigms; (2) Long Chain-of-Thought Supervised Fine-Tuning (L-CoT SFT) on expert-validated reasoning-and-code samples to emulate proactive risk-aware thinking; and (3) Robustness-Aware Group Relative Policy Optimization (R-GRPO), a reinforcement learning phase optimizing a weighted reward for syntax correctness, robustness (via shellcheck), and format correctness. We evaluate on BashBench, a new benchmark of 952 real-world tasks (773 single-line, 179 multi-line). BashCoder-R1 achieves SyntaxPass (100.00%/94.97%), RobustWarnRate (4.01%/16.47%), RobustPass (95.99%/79.33%), FuncRate (93.01%/93.85%), and FullRate (90.04%/73.18%) for single-line/multi-line tasks, outperforming the strongest baseline DeepSeek-V3.2 (Reasoning) by 37.82% and 20.18% in FullRate. Human evaluation on Functionality, Robustness, and Clarity further confirms BashCoder-R1 achieves the highest quality ratings.

Repository-level performance optimization remains challenging for LLM-based coding agents. In addition to preserving program semantics, optimization requires (i) diagnosing performance bottlenecks and (ii) validating improvements under noisy, workload-dependent measurements. Existing approaches are largely instance-driven: they rely on local profiling signals, follow a single optimization trajectory, and provide limited support for transferring optimization knowledge across repositories. As a result, agents can overfit incidental hotspots and underuse broadly effective optimization strategies.

We present MoKOpt, a repository-level optimization framework that casts optimization as a Mixture-of-Skills (MoK) problem. MoKOpt comprises three mechanisms. (1) It distills expert optimization patches into reusable \emph{skill cards} that encode applicability conditions and transformation intent. (2) Given a profiling report, it dispatches candidate skills as independent patch-generation branches, enabling systematic exploration of alternative hypotheses. (3) It enforces phase isolation via phase-specific state and code context, reducing cross-branch interference.

We evaluate MoKOpt on repository-level optimization tasks across multiple base agents and language models. MoKOpt consistently improves optimization success by combining reusable optimization knowledge, diversified search, and execution-grounded validation, moving beyond single-trajectory, instance-specific optimization. Across settings, MoKOpt outperforms strong agentic optimization baselines, achieving up to a +250.90% advantage relative to the maintainer-written expert patch.

通用大语言模型直接将自然语言表述的实时控制需求转换为嵌入式 C 代码的开发模式，存在语义黑盒不可解释、需求歧义后置、模型幻觉引入逻辑错误、代码耦合严重难以维护等核心缺陷，难以满足安全关键嵌入式软件可信开发要求。现有研究大多跳过形式化中间模型，直接完成自然语言到程序代码的端到端映射；少量 LLM 辅助有限状态机生成工作仅产出图形化 UML 模型，缺少标准化、可仿真、中文可读的形式化载体，无法实现需求歧义前置消除。 本文提出一套以状态迁移矩阵（STM，State Transition Matrix）为中间层的全链路可信代码生成方案，核心理论创新为利用微调大模型完成上下文相关自然语言（CSL）需求向上下文无关语言（CFL） STM的自动转换，从语言学层面消解自然语言固有的语义二义；依托工业级EDA工具 ZIPC开展全状态路径遍历迭代验证，提前检出需求遗漏、状态互斥、时序冲突等逻辑缺陷；将 STM模型 内极小粒度 Action 动作拆分后分段生成 C 函数，规避大模型一次性生成完整代码的幻觉风险，最终由 ZIPC 基于已验证的形式化模型确定性导出嵌入式工程代码。 选取 CD 播放器实时控制系统作为完整工程案例，落地 “需求文档→微调 LLM 生成 STM→ZIPC 仿真迭代修正→分段生成动作函数→工具导出整机 C 代码” 全流程。对比实验结果表明：相较于通用 LLM 直译代码方案，本文方法需求缺陷前置检出率达到 100%，完全消除 AI 逻辑幻觉错误，需求至代码双向追溯覆盖率 100%，人工调试修复工时降低 83.1%。本方法为大模型辅助程序生成提供可解释形式化中间层新思路，适用于车载、工业控制、消费电子等嵌入式实时控制系统开发，契合程序语言、形式化规约、可信代码生成领域研究方向。

Behavior trees (BTs) are widely adopted in the field of agent control, particularly in robotics, due to their modularity and reactivity. However, constructing a BT that meets the desired expectations is time-consuming and challenging, especially for non-experts. This paper presents BtBot, a multi-modal sketch-based behavior tree synthesis technique. Given a natural language task description and a set of positive and negative examples, BtBot automatically generates a BT program that aligns with the natural language description and meets the requirements of the examples. Inside BtBot, an LLM is employed to understand the task’s natural language description and generate a sketch of the task execution. Then, BtBot searches the sketch to synthesize a candidate BT program consistent with the user-provided positive and negative examples. When the sketch is proven to be incapable of generating the target BT, BtBot provides a multi-step repairing method that modifies the control nodes and structure of the sketch to search for the desired BT. We have implemented BtBot in a prototype and evaluated it on a benchmark of 70 tasks across multiple scenarios. The experimental results indicate that BtBot outperforms the existing BT synthesis techniques in effectiveness and efficiency. In addition, two user studies have been conducted to demonstrate the usefulness of BtBot.

(This paper has been published at OOPSLA 2025.)

Deductive verification scales to large software systems through modular reasoning, where formal contracts summarize the behavior of individual functions and enable their independent verification. Its central bottleneck is specification synthesis: constructing the contracts required for modular verification. Recent advances in large language models (LLMs) have enabled automated specification synthesis at unprecedented scale. However, existing approaches remain fundamentally bottom-up, requiring callees to be verified before their callers. This dependency limits parallelism and provides no principled mechanism for resolving interprocedural inconsistencies that propagate across call chains.

We present Verdict, a multi-agent framework for parallelizing modular deductive verification of large-scale programs. Verdict is built on two key principles. First, assumption-based parallel specification synthesis assigns an agent to each function and allows it to proceed immediately using assumed contracts for its callees, enabling verification to proceed in parallel across the program. Second, bidirectional interprocedural conflict reconciliation resolves the inconsistencies introduced by these assumptions: when a synthesized contract contradicts an assumption, agents propagate the necessary revisions both up and down the call graph until the contracts converge. Experimental results on real-world C programs demonstrate that Verdict synthesizes higher-quality specifications than existing approaches while substantially reducing verification time. In particular, Verdict is the first approach that scales to the complete 20,000-line X.509 parser, ruling out nearly all the potential runtime errors within hours, whereas prior tools fall far short even after days of execution.

Quantum-classical hybrid programs must coordinate pulse generation, measurement, and classical updates while the quantum state continues to evolve. This makes timing a semantic concern: classical instructions consume real time, and their latency can shift later pulse emissions away from the intended schedule. We present a pulse-level domain-specific language (DSL) for quantum-classical control programs together with a timing semantics that specifies the intended schedule of waveform emission and explicit waiting. This semantics exposes a mismatch with low-level execution: after lowering to a conventional control processor, loop updates, branches, and parameter arithmetic take processor cycles that are absent from the ideal pulse-level schedule. To close this gap, we introduce timing fusing, a compiler pass that operates on a timing-aware control-flow graph (t-CFG) to preserve the pulse-level timing semantics by redistributing wait durations to absorb classical execution latency. We validate the approach in an end-to-end prototype toolchain with timing output, hardware-level simulation, and calibration-oriented test programs.

Probabilistic programming provides a high-level paradigm for specifying statistical models as executable programs with built-in randomness and conditioning. Existing inference techniques, however, typically calculate posterior distributions over program states at fixed time points—most often at termination—and therefore fail to capture the temporal evolution of a program’s probabilistic behavior. In this work, we introduce \emph{temporal posterior inference} (TPI), a framework for posterior reasoning about entire execution traces by computing the posterior probability that a conditioned probabilistic program satisfies an $\omega$-regular temporal specification. To obtain rigorous quantitative guarantees, we develop a method that computes lower and upper bounds on these satisfaction probabilities at increasing levels of approximation, and we prove a convergence theorem establishing that the bounds are asymptotically sound in the limit for the target TPI. Our approach decomposes Rabin acceptance conditions into persistence and recurrence components, and constructs stochastic barrier certificates that bound each component asymptotically. We implement our approach in a prototype tool, \textsc{TPInfer}, and evaluate it on a suite of benchmarks, demonstrating effective inference over rich temporal properties in probabilistic models.

Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define assertion logic and program logic specifically crafted for QEC programs and establish a sound and weakly relatively complete proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.

Quantum oracles are essential to many quantum algorithms, and their specifications may involve recursive control flow that depends on runtime quantum data. However, existing reversible compilation frameworks provide limited support for such quantum-controlled recursive structures.

We present ReOC, a compilation framework that transforms high-level recursive oracle specifications with quantum control flow into reversible quantum programs. The framework comprises RQIMP, a high-level imperative source language for specifying recursive oracles, and a method of compiling programs in that language into (\RQC^{++}), an existing high-level quantum recursive language with quantum control flow. In this way, we avoid the tedious and error-prone process of directly writing quantum oracles in (\RQC^{++}).

To manage static storage under dynamic quantum control, ReOC uses an indexed static-register discipline to isolate live variables across recursion layers, enabling safe register reuse while controlling quantum storage usage. Furthermore, to address the exponential time blow-up caused by naive uncomputation in recursive settings, ReOC employs a recursion-aware uncomputation strategy: temporary variables from recursive calls are cleaned using deferred strategies to control time overhead, while those from non-recursive statements are cleaned eagerly to reduce space usage. For linear recursion, this strategy yields overhead linear in recursion depth, parameterized by the per-layer register footprint and primitive-operation costs. Finally, we provide a mathematical proof of compilation correctness from RQIMP to (\RQC^{++}), establishing semantic preservation and correct uncomputation of temporary quantum variables.

Relational program logics reason about executions of two programs and are particularly well-suited to security of cryptographic schemes and generalization properties of machine-learning. In the quantum setting, they have been used to reason about quantum processes and quantum security, but the existential nature of coupling-based reasoning makes completeness challenging. We overcome this challenge by leveraging duality theorems from quantum optimal transport. We first introduce a quantitative relational Hoare logic for finite-dimensional quantum programs, whose assertions range over an infinitary extension of positive semidefinite operators. The logic is sound and complete for bounded postconditions and almost surely terminating programs, and it provides a complete embedding of a relational Hoare logic with projective assertions. We then extend this approach to infinite-dimensional quantum and classical-quantum programs and a general form of assertions. Assertions are modeled as self-adjoint unbounded linear relations, which simultaneously support quantitative and qualitative reasoning. New convergence theorems and infinite-dimensional duality theorems for infinite-dimensional quantum states yield sound and complete relational program logics for almost surely terminating programs with unbounded assertions. This presentation synthesizes results from two joint works published in the LICS 2025 and LICS 2026.

Several recently proposed program logics have incorporated notions of underapproximation into their design, enabling them to reason about reachability rather than safety. In this paper, we explore how similar ideas can be integrated into an expressive type and effect system. We use the resulting underapproximate type specifications to guide the synthesis of test generators that probe the behavior of effectful black-box systems. A key novelty of our type language is its ability to capture underapproximate behaviors of effectful operations using symbolic traces that expose latent data and control dependencies, constraints that must be preserved by the test sequences the generator outputs. We implement this approach in a tool called Clouseau, and evaluate it on a diverse range of applications by integrating Clouseau’s synthesized generators into property-based testing frameworks like QCheck and model-checking tools like P. In both settings, the generators synthesized by Clouseau are significantly more effective than the default testing strategy, and are competitive with state-of-the-art, handwritten solutions.

A desired but challenging property of compiler verification is compositionality, in the sense that the compilation correctness of a program can be deduced incrementally from that of its substructures ranging from statements, functions, and modules. This article proposes a novel compiler verification framework based on denotational semantics for better compositionality, compared to previous approaches based on small-step operational semantics and simulation theories. Our denotational semantics is defined by semantic functions that map a syntactic component to a semantic domain composed of multiple behavioral \emph{sets}, with compiler correctness established through behavior refinement between the semantic domains of the source and target programs. The main contributions of this article include proposing a denotational semantics for open modules, a novel semantic linking operator, and a refinement algebra that unifies various behavior refinements, making compiler verification structured and compositional. Furthermore, our formalization captures the full meaning of a program and bridges the gap between traditional power-domain-based denotational semantics and the practical needs of compiler verification. We apply our denotation-based framework to verify the front-end of CompCert and typical optimizations on simple prototypes of imperative languages. Our results demonstrate that the compositionality from sub-statements to statements, from functions to modules, and from modules to the whole program can be effectively achieved.

Verifying the functional correctness of real-world code with complex algorithms can be decomposed into two layers: verifying that the concrete code refines an abstract algorithmic description, and proving the correctness of the formal description. However, in practice the two layers do not stay cleanly separated. For example, in the verification of the Knuth-Morris-Pratt (KMP) algorithm, the implementation correctness proof often re-establishes algorithm properties that have already been proved, as the concrete implementation relies on invariants that the traditional two-layer method provides no mechanism to transfer. This makes it difficult to clearly separate the concerns of algorithm correctness and implementation correctness. In this pearl, we show how a clean separation can be achieved within the two-layer method by combining two simple ideas: expressing implementation correctness as a relational Hoare quadruple, and introducing assertion annotations into the abstract program to capture key invariants. Properties established in the algorithm proof are thereby transferred directly to the implementation proof, eliminating the need to re-prove them. We demonstrate the effectiveness of this approach through non-trivial case studies, including the Knuth-Morris-Pratt pattern-matching algorithm and the depth-first search algorithm, showing that it leads to simpler proofs and a more modular verification process.

This paper presents a mechanized formal semantics for the Linux eBPF instruction set architecture (ISA). We develop a small-step semantics in Rocq that faithfully formalizes all 153 sequential in-kernel instructions of the eBPF ISA. The semantics is fully executable and has been validated against the official Linux eBPF test suite. This extensive testing revealed inconsistencies in our original formalization. Using this semantics, we have designed, implemented, and verified the soundness of the bit-level abstract domain employed by the Linux eBPF verifier. Our semantics also complements the existing Linux eBPF documentation by providing a rigorous formal specification. During the formalization process, we have discovered previously unknown bugs in the Linux eBPF implementation, and developed new verifier optimizations; all of these changes have been upstreamed to the latest version of the Linux kernel.

Verifying stateful software systems remains challenging due to complex control structures and intricate state interactions, often necessitating pre-existing behavioral models. We introduce Seal, an abstract interpreter that automatically derives sound and precise symbolic finite automata models. In tests on real-world applications, Seal generates sound and precise automata within minutes and, when employed in dynamic model checking, achieves 1.6×–3.4× code coverage compared to the state of the art. These findings demonstrate that Seal can effectively connect code to model-based verification for stateful software systems.

We propose a novel framework that provides constructive feedback to an LLM in the “guess-and-check” paradigm by formally verifying its own thinking process and detecting local reasoning errors. We apply this framework to the loop invariant synthesis problem. We prompt the model to produce a step-by-step natural language proof justifying its thinking process for the failed verification condition of its generated loop invariants. Then, we use an LLM to translate the reasoning steps into first-order logic implications, which can be checked automatically. An invalid implication pinpoints the exact logical flaw in the LLM’s thinking process, which we then use to construct targeted feedback for refinement. We have implemented our approach in a tool called LORIS and evaluated it on a main benchmark suite of 460 C programs and an additional benchmark suite of 50 C programs each of which involves non-linear properties. On the main benchmark suite, LORIS solved 445 of the programs and achieved an overall success rate of 93.1%. LORIS also demonstrates robustness on the challenging non-linear benchmark suite.

Symbolic execution faces the challenge of generating valid inputs when analyzing the program with complex input formats. Token-based symbolic execution can partially tackle this challenge but is still doomed by the difficulty of passing input checking and failing to analyze the code after input checking. We propose Lase, an online input grammar synthesis aided symbolic execution method, to generate valid inputs for improving the effectiveness of symbolic execution. Inside Lase, we propose an input grammar-oriented search strategy and a token-level grammar synthesis method. The search strategy selects the paths to cover more syntax rules in priority. The token-level grammar synthesis improves the synthesized grammar’s precision and completeness while ensuring efficiency. The experimental results on real-world parsing programs with complex input grammars demonstrate that Lase can improve the coverage of parsing code and generate more valid inputs to improve the coverage of functionality code significantly. Furthermore, compared with the state-of-the-art grammar synthesis methods, the grammars learned by Lase have better precision and recall on most benchmark programs.

This paper is accepted for publication at OOPSLA 2026.

Verifying concurrent programs under diverse memory models has long been a central challenge. The rapid emergence and evolution of memory models highlight the need for a configurable verification approach. In this paper, we present an efficient and configurable decision procedure for verifying programs under user-specified memory models. Rather than eagerly translating the complex relation computations defined in a memory-model specification into SMT, our approach embeds a dedicated, model-configurable theory solver into the DPLL(T) loop. The solver incrementally computes partial-order relations and checks consistency on demand, thereby enabling efficient verification while avoiding unnecessary SMT encodings.

A key difficulty is that memory-model specifications may contain non-monotonic constructs that introduce negative dependencies: such constructs can invalidate previously detected conflicts and undermine DPLL(T)’s conflict learning. We identify the sources of non-monotonicity and propose a monotonization transformation that rewrites non-monotonic constructs into equivalent, monotonic formulations. Experiments across multiple memory models show that this design achieves promising performance while providing flexible support for memory models.