跳到正文
研踪PaperTrail

论文库

检索计算机领域论文，按研究方向、作者或关键词筛选。

部分采集异常
正在读取账号与研究记录…

全站更新概况

+0新增论文
+0其中 AI 相关
+2已有论文修订
+100新增 AI 导读

arXiv 最近完成扫描：2026-11-15 08:47 · 全站最近入库：2026-11-14 15:09各信源进度 →

统计口径与数据新鲜度

统计 2026-11-14 08:56 — 2026-11-15 08:56（北京时间） · 点击数字查看对应简报；AI 相关包含在新增论文内。

最近完成检查：2026-11-15 08:47最近发现新增版本：2026-11-14 15:09库内论文最新更新时间：2026-11-13 02:59

每分钟刷新已保存的数据。空检查不代表采集异常；新收录可能包含历史论文。AI 导读按新增版本计数。

23,348 已收录论文19,580 AI 相关6,729 有修订112 HF 社区发现

浏览论文库

研究日报 / 周报 →按信源浏览 →

时间范围跟随排序：版本更新、本站收录或首次发表。最新收录可能包含历史论文。部分信源异常，查看状态 →

找到 114 篇论文 · 按版本更新时间排序上轮扫描起点 2026-11-15 08:46（北京时间）
版本更新 · v2arXiv:2602.03777

Statically Verifying Well-Definedness of Separately Compiled Attribute Grammars

Federico Bruzzone, Walter Cazzola, Luca Favalli

原文摘要

The development of programming languages involves complex theoretical and practical challenges, particularly when addressing modularity and reusability through language extensions. While language workbenches aim to enable modular development under the constraints of the language extension problem, one critical constraint--separate compilation--is often relaxed due to its complexity. However, this relaxation undermines artifact reusability and integration with common dependency systems. A key difficulty under separate compilation arises from managing attribute grammars, as extensions may introduce new attributes that invalidate previously generated abstract syntax tree structures. Existing approaches, such as the use of dynamic maps in the Neverlang workbench, favor flexibility at the cost of compile-time correctness, leading to potential runtime errors due to undefined attributes. This work addresses this issue by introducing nlgcheck, a theoretically sound static analysis tool based on data-flow analysis for the Neverlang language workbench, which detects potential runtime errors--such as undefined attribute accesses--when separately compiled language components are composed, before the resulting language is ever run, thus preserving separate compilation while maintaining strong static correctness guarantees. Experimental evaluation using mutation testing on Neverlang-based projects demonstrates that nlgcheck effectively enhances robustness without sacrificing modularity or flexibility and with a level of performance that does not impede its adoption in daily development activities.

cs.PL · cs.SE

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.12315

Beating Rytter's Bound: All-Pairs CFL Reachability in $O(n^3(\log\log n)^2/(\log n)^2)$ Time

Rupak Majumdar

原文摘要

Context-free reachability and 2NPDA recognition are fundamental problems in program analysis and language theory. Despite years of effort, the best algorithms for these problems run in time $O(n^3/\log n)$ on a word RAM model; they are based on an observation of Rytter in 1985 for 2NPDA which was adapted for CFL reachability by Chaudhuri in 2008. No better algorithm has been designed since. We give the first improvement to Rytter's algorithm. For both all-pairs context-free reachability and 2NPDA recognition, we show a deterministic algorithm running in $O(n^3(\log\log n)^2/(\log n)^2)$ time and $O(n^{2+ε})$ words of space for every fixed $0<ε<1$ on a word RAM. Our improvement is based on a new data structure that reports set differences using batched maintenance of exact intersection counts, allowing saturation to skip regions that contain no new reachability information.

cs.PL · cs.FL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2412.17330

EcoSearch: A Constant-Delay Best-First Search Algorithm for Program Synthesis

Théo Matricon, Nathanaël Fijalkow, Guillaume Lagarde

原文摘要

Many approaches to program synthesis perform a combinatorial search within a large space of programs to find one that satisfies a given specification. To tame the search space blowup, previous works introduced probabilistic and neural approaches to guide this combinatorial search by inducing heuristic cost functions. Best-first search algorithms ensure to search in the exact order induced by the cost function, significantly reducing the portion of the program space to be explored. A key limitation of existing best-first search algorithms is that they slow down over time: the delay between outputting successive programs grows with the number of programs already generated. We ask whether best-first search algorithms with constant delay exist. We design Eco Search, a new best-first bottom-up search algorithm. It combines the cost tuple representation of Bee Search with the per non-terminal data structures of Heap Search, thanks to a new frugal expansion strategy, and it uses bucket queues instead of priority queues, which is possible because the costs stored in each queue always lie in a window of constant width. We prove that Eco Search is the first constant-delay best-first search algorithm for pre-generation cost functions. Experimentally, we evaluate Eco Search on two classic program-synthesis benchmarks (DeepCoder and FlashFill) and observe that Eco Search solves 12% to 70% more tasks than its predecessors, and reaches the number of tasks they solve 1.6 to 3.2 times faster. This shows that constant delay can be achieved for best-first search in program synthesis, and that it makes a difference in practice.

cs.LG · cs.AI · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2610.38983

Beyond atol and rtol: Sound Test Oracles for Low-Precision GPU Kernels

Xinyi Shi

原文摘要

Low-precision GPU kernels are commonly tested against a reference using hand-picked absolute and relative tolerances. Legitimate numerical error varies with the input, format and precision plan, so a fixed tolerance trades false alarms for missed faults. We present numoracle, which derives per-element acceptance regions from precision-annotated reference programs. Its calculus tracks shared rounding errors, provenance-ordered products, block-scaled quantizers and calibrated math-library errors. A rounding-interval check detects faulty stores that symmetric bounds can admit. Soundness is conditional on explicit rounding, hardware, domain and implementation assumptions; a fixed-input mode removes the zero-mean rounding assumption. We evaluate 13 Triton operators from Liger-Kernel, Unsloth and vLLM on two GPU generations. The main campaigns produce no false alarm on 33,960 correct-kernel and behavior-preserving-variant runs per GPU. Under input shift, the GPU campaigns record no false alarm while tuned tolerances flag up to 30% of correct runs; final-version reference checks identify inputs without complete finite-range certificates. On the RTX PRO 6000, numoracle kills 116 of 124 effective mutants, versus 59-83 for four fixed baselines. Among 400 tuned tolerance configurations, requiring at most 1% false alarms in every evaluated Liger input group permits at most 31 of 53 main-mutant kills, versus numoracle's 50. Historical replays expose accuracy faults in eight change pairs without rejecting their matched corrected controls; a ninth change concerns rounding parity.

cs.MS · cs.PL · cs.SE

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.11899

How Far Must a Test Explore? Certifying Composable Read-Write Interfaces from Their Own Random Edits

Jiaxuan Guo, Xingyu Ren, Jingxin Yang, Youran Sun, Haizhao Yang

原文摘要

Random tests of stateful code check laws, like reading back a written value, at states that random writes reach. The laws hold at every state exactly when the code behaves like a record with hidden data, so a pass is taken as evidence. This can fail: the laws can hold at every sample while the code is far from any record. The laws are local, but behaving like a record is global. Self-testing and stability theorems bridge this gap when the query distribution is controlled by the tester or preserved by the tested maps, but here it is generated by the tested writes, which need not be invertible. We ask how far a test must explore. An interface has $m$ binary variables, each with a read and two writes; in a record, reads return their bits and writes set only their bits. Samples are the ends of geometric runs of mean $\ell$ of uniformly random writes from a start distribution; a tester adds its own write chains of depth $d$. The distance is the least, over records with hidden data, of the largest probability that a read or write differs from it at a sample. From one start state, law checks at $O(m^2\log m/ε)$ samples certify, at fixed confidence, any threshold $ε$ after geometric runs of every positive mean, while runs of fixed positive length can pass at distance $1/2$. For the worst start distribution, take $ε=m^{-β}$ with fixed $0<β\le1$. For $d\le cm$ with fixed $c<1/2$, a polynomial budget of samples and writes exists exactly when $\ell=Ω(m)$, where law checks suffice. With no runs, the least depth for this budget is $(1/2+o(1))m$. Counting samples alone, in the worst case at $ε=1/(32m)$ and $d\le m/16$, the critical mean for a polynomial budget is $Θ(m\log(m/d)/\log m)$, by exhaustive search. So one start state needs only law checks, and the worst case at these thresholds needs exploration linear in $m$ if writes are counted.

cs.DS · cs.LG · cs.PL · cs.SE

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2611.06079

TauLang: A Language and Compiler for Space-Time Programming on Statically Scheduled Accelerators

Xuxiao Yang, Junchi Wu, Yuqi Peng, Feiyang Wu, Zhuoran Li, Wei Kong, Shuo Tao, Dongyi Fan 等 14 位作者

原文摘要

Statically scheduled accelerators such as Groq's Tensor Streaming Processor (TSP) achieve low-latency large language model inference by stripping dynamic synchronization hardware from the chip. With no caches, arbiters, or hardware schedulers, the compiler must fix the exact slice and issue cycle of every operation, so when an operation runs is a condition for correctness. Existing kernel languages cannot target such machines because they rely on hardware to resolve cycle timing and instead encode schedules implicitly in code structure. We present TauLang, a kernel language and compiler that makes time a first-class citizen of the program. The programmer schedules operations, loops, and composed kernels with parameterized explicit times, so exploring schedules means changing parameter values rather than rewriting code. TauLang validates explicit times algebraically in TauIR, its timed intermediate representation. It then solves tensor placement and cycle scheduling jointly in an integer linear program, using explicit times to group connected operations into timing clusters that prune the search space. On a cycleaccurate model of a TSP-like machine, joint search achieves a $1.40\times$ latency speedup across ten kernels over a space-first flow. A few explicit time pins keep latency within one cycle of the untimed schedules and scale joint search to 1,636 GEMM blocks, whereas untimed search finds no schedule at 32.

cs.PL · cs.AR

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2501.15156

Quantifier Elimination and Craig Interpolation, Quantitatively

Kevin Batz, Joost-Pieter Katoen, Nora Orhan

原文摘要

Quantifier elimination (QE) and Craig interpolation (CI) are central to various state-of-the-art automated approaches to hardware- and software verification. They are rooted in the Boolean setting and are successful for, e.g., first-order theories such as linear rational arithmetic. What about their applicability in the quantitative setting where formulae evaluate to numbers and quantitative supremum/infimum quantifiers are the natural counterpart to Boolean quantifiers? Applications include establishing quantitative properties of programs such as bounds on expected outcomes of probabilistic programs featuring non-determinism and analyzing the flow of information through programs. In this paper, we present, to the best of our knowledge, the first QE algorithm for possibly unbounded, $\infty$- or $(-\infty)$-valued, or discontinuous piecewise linear quantities. They are the quantitative counterpart to linear rational arithmetic, and they are a popular quantitative assertion language for probabilistic program verification. We provide rigorous soundness proofs as well as upper bounds on the size of the output. Moreover, we present two applications of our QE algorithm. First, our algorithm yields a quantitative CI theorem: Given arbitrary piecewise linear quantities $f,g$ with $f \models g$ (i.e., $f$ is at most $g$ at every variable valuation), both the strongest and the weakest Craig interpolants are quantifier-free and effectively constructible. Such interpolants lie between the two quantities and use only their common free variables. Second, we apply our QE algorithm to computing minimal and maximal expected outcomes of loop-free probabilistic programs featuring unbounded non-determinism, and to checking inductivity of candidate upper bounds on minimal and maximal expected outcomes of probabilistic loops featuring unbounded non-determinism.

cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2610.11991

Quantitative Verification of Infinite-State Networks

Dhruv Nevatia, David Basin

原文摘要

Many network protocols and distributed systems combine recursion, unbounded local state, and quantitative behaviour such as cost, latency, or reliability. Existing decidability results for networks of pushdown systems are largely qualitative, and do not extend to quantitative analyses, which must jointly track traces and weights. We present a framework for the quantitative verification of acyclic networks of weighted pushdown systems. Finitely summarising a recursive network component requires collapsing the infinite family of runs obtained by pumping its nested loops, and doing so exactly, rather than by over-approximation, is a standing difficulty. We give a class of weight domains where this is possible: pumping semirings, those in which the weights accumulated by such a family collapse to a closed form; informally, the domain must be unable to count iterations. The class admits domains with infinite ascending chains, such as the arctic semiring and downward-closed languages. Over these, we give a terminating saturation algorithm computing quantitative reachability exactly, resting on two ideas: segment tree algebras, a compositional representation of runs, and thermal extensions, which symbolically separate accelerated weights so that further acceleration remains exact. We use this to compute upward and downward closures of context-free languages uniformly, and to lift the algorithm to acyclic networks over "thin" pumping semirings, yielding the first quantitative safety and reachability analyses for networks of pushdown systems.

cs.FL · cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2606.07665

AgentCompile: An LLM-Guided Compiler for Direct CUDA Inference

Xuanzhe Li, Ziyan Weng, Zhiyu Zhu, Junhui Hou

原文摘要

Transformer inference increasingly relies on specialized compiler and runtime support, while recent LLMs can generate nontrivial CUDA kernels. However, unconstrained generation guarantees neither correctness nor performance. We present \textsc{AgentCompile}, an LLM-guided CUDA inference compiler that combines two complementary uses of LLMs. First, the LLM provides advisory metadata for compiler-derived region summaries and bounded candidate spaces. The compiler then instantiates template-based CUDA candidates, validates correctness, selects implementations by measured latency, and falls back when specialization is unsupported or unprofitable. Second, under compiler-defined contracts, the LLM directly generates five classes of decode-critical kernels to accelerate inference, prompted by distilled optimization principles. \textsc{AgentCompile} integrates these kernels into a serving runtime with paged KV cache, continuous batching, preemption, chunked prefill, and bucketed full-step CUDA Graph replay. Across six evaluated model families, \textsc{AgentCompile} achieves speedups of \textbf{2.23--6.98$\times$} over PyTorch eager for single-request generation, and \textbf{1.04--1.16$\times$} over vLLM for both single-request generation and multi-request serving. Our code is publicly available at https://github.com/veneno1213822/AgentCompile.

cs.PL · cs.AI

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.11117

Keel: A Verified In-Kernel Proof Checker for Proof Carrying BPF

Yalu Cai, Tung-Che Chang, Santosh Nagarakatte

原文摘要

Recent systems such as the eBPF Certificate Framework (BCF) and Proof-Carrying BPF address the imprecision in the Linux eBPF verifier with proof-carrying code. When the verifier's abstract domains cannot prove a safety condition, an in-kernel proof checker checks an untrusted user-space refutation proof. A single bug in this checker can compromise the security of the entire kernel. While formalizing BCF's in-kernel checker, we discovered 13 bugs such as unsound rewrite rules, silently unchecked proof steps, and memory safety errors. We demonstrate that forged certificates can trick the kernel to accept arbitrary unsafe eBPF programs. To address this problem, we propose Keel, a formally verified in-kernel proof checker for the Linux eBPF verifier. First, we specify the checker as a pure functional program in Lean and prove its soundness against bit-vector semantics. We decouple the steps of the proof certificate checker from the mathematical rewrite rules, which enables us to extend the rewrite rules without the need to change the checker. Second, we implement the checker in EmbC, a deeply embedded C fragment, and prove that our C implementation refines the functional specification without undefined behavior or memory leaks. Third, using an amortized potential argument, we prove linear time and memory bounds for the C checker. Keel is correct-by-construction while also being faster than the BCF checker inside the kernel, 1.3X in total and 2.0X on the slowest 1.4% of certificates.

cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v13arXiv:2602.16291

A Calculus of Inheritance

Bo Yang

原文摘要

Just as the $λ$-calculus is a pure functional programming language built from three primitives (abstraction, application, variable), we present inheritance-calculus, a pure declarative programming language built from three primitives (mixin, definition, reference). We introduce multi-target $\mathtt{this}$ to solve the problem that inheritance conflicts with modularity, and thereby unify object-oriented and configuration constructs: modules, classes, objects, methods, fields, and locals become a single mixin abstraction, and inheritance becomes simply set union, the deep merge of configuration languages. Consequently, composition is commutative, idempotent, and associative, structurally eliminating the multiple-inheritance linearization problem; the inheritance relation has substitutability; every path of every program can be inherited and extended; every subtree can be split into parts that, inherited together, behave as the whole; and programs have no side effects and cover every input. We call these properties modularity by construction. The calculus has no functions, yet it macro-expresses the lazy $λ$-calculus and is more macro-expressive than it in Felleisen's sense. Its semantics is first-order, denotational, and evaluated by tabling, even for cyclic inheritance hierarchies. Inheritance-calculus is distilled from MIXINv2, an implementation in which the same code acts as different function colors and ordinary arithmetic agrees with the relational semantics of logic programming.

cs.PL · cs.SE

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.11057

Symbolic Synthesis with Token-Level LLM Guidance

Derek Egolf, Stavros Tripakis

原文摘要

We propose a synergistic combination of classical program synthesis techniques and contemporary large language models (LLMs) to solve the problem of recursive program synthesis from first-order logic specifications. Our approach leverages the strengths of both paradigms: we use LLMs as a source of statistical bias to guide the search for a correct program. At the same time we use techniques from classical synthesis to short-circuit on semantically incorrect prefixes and to avoid sampling semantically equivalent responses. The statistical bias is derived from the next-token distribution of an LLM, which is highly context-dependent. We operate with the understanding that (1) there is some class of synthesis instances that can be discharged by small models and symbolic tools, and (2) every other instance can be decomposed into these instances. Therefore, our intention is to expand the reach of small, open-weight LLMs and symbolic synthesis techniques, not to compete with proprietary frontier models on every possible instance. These are different tools for different jobs. In our experimental evaluation, we find that our method solves more benchmarks than either small LLMs or classical synthesis techniques alone. Our method solves 30/32 benchmarks using only a Qwen2.5 model with 32 billion parameters. Qwen2.5 solves 0 benchmarks on its own, and only solves a few additional benchmarks when combined with traditional constrained decoding techniques.

cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2609.38242

A Calculus for Units of Measure with Conversion

Eric Allen

原文摘要

Programs that compute with physical quantities often need to convert between units of measurement, and as the Mars Climate Orbiter showed, these conversions can be a rich source of errors. Meanwhile, typed unit calculi, our most rigorous formalisms for checking physical units in a program, have excluded unit conversions. Through this exclusion, they have established a powerful property: well-typed programs are invariant under rescaling (no program can depend on how big a meter is). But losing the ability to convert between units is a significant cost. In contrast, practical languages provide conversion but no invariance theorem. We present $Λ_S$, a typed lambda calculus with conversion, quantification over units and dimensions, and vectors and linear maps with per-component units, and we determine exactly how much invariance survives conversion. For terms without unit constants we prove two abstraction theorems: (i) a convert-free term is invariant under every rescaling; (ii) a term with conversions is invariant under every rescaling that scales all units of one dimension by the same factor. The condition in (ii) cannot be weakened: under any other rescaling, some conversion of a nonzero value is not invariant. For first-order programs, a verified decision procedure returns one of three verdicts: it certifies that no error in the declared conversion factors can change the program's answer, names the accumulated ratio through which such an error would scale it, or declines. A verified checker decides whether unit declarations are consistent and determine every conversion factor, and extracts each factor exactly. We also prove adequacy, erasure, and the $n$-variable Pi theorem of dimensional analysis with conversion. Every theorem is mechanized in Lean 4, and the evaluator compiles to a native binary.

cs.PL · cs.LO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.10855

Representing Tensors as Compositions for Efficient Computation on Sparse and Structured Data

Valérian Rey, Praneth Paruchuri

原文摘要

We propose a new mathematical formalism in which all kinds of tensors and of operations on those tensors are represented as simple function compositions. Tensors are functions from indices to values. An element-wise operation (e.g. an activation function) is a composition with a function applied to values; re-indexing (e.g. reshape, transposition) is a composition with a function applied to indices; and a reduction is a composition with both an index function, mapping each index to several indices, and a reduction operation (e.g. product, sum, max). Combined with tensor stacking, these compositions can represent most interesting kinds of tensors (e.g. dense, jagged, all kinds of sparsity patterns, matrix factorizations), as well as lazy versions of almost every operation available in modern tensor computation frameworks, including einsums between tensors of any kind. Identities between compositions can then be used to rewrite such expressions into equivalent ones, without evaluating them. For instance, the product of two sparse matrices can be rewritten so that only products between non-zero values are computed, turning a sparse problem into a dense one. Using this algebra as the intermediate representation of a tensor computation engine would shift the focus from defining operations on tensors (e.g. einsum between sparse tensors) to defining an algebra on index functions. This should reduce the codebase complexity from $\mathcal{O}(mn^2)$, with $m$ the number of binary operations between tensors and $n$ the number of tensor types, to $\mathcal{O}(m + k^2)$, with $k$ the number of types of index functions. A draft implementation of a tensor computation framework based on this algebra is publicly available.

cs.LG · cs.MS · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v7arXiv:2603.13334

Lipschitz-Based Robustness Certification Under Floating-Point Execution

Toby Murray

原文摘要

Lipschitz-based certification checks a neural network's robustness with a small numerical computation: milliseconds per input, and small enough to be formally verified. Its soundness is proved for execution in real arithmetic, whereas deployed networks execute in floating point, so rounding must be accounted for in the network and in the certifier itself. We show that the conservatism of Lipschitz-based certification does not absorb the rounding in the network's execution: we exhibit counterexamples to a formally verified real-arithmetic certifier that computes in exact arithmetic, and show that an adversary who controls the weights can make it issue false certificates for ordinary test images at standard perturbation bounds. We present the first Lipschitz-based certification method that is both efficient and sound with respect to floating-point execution. It keeps the real-arithmetic network's Lipschitz constant and bounds separately how far the floating-point outputs can depart from the real-arithmetic ones, through a compositional theory of the deviation that also rules out overflow; pre-deployment measurements of a high-precision execution tighten the bound. Its spectral norms come from a float64 Gram iteration proved never to under-estimate the true norm. We mechanise the theory in Rocq and implement it in a certifier, evaluated on dense image, tabular and many-class classifiers. It rejects every certificate a counterexample refutes and certifies entire test sets at milliseconds per instance on a CPU, losing relatively few real-arithmetic certificates, many of which the measurement reclaims. At float32, ERAN's GPUPoly, to our knowledge the only other public floating-point-sound verifier for networks of our size, loses most of its certificates on most of our models to its own rounding accounting; ours does not, and is more than an order of magnitude faster.

cs.LG · cs.CV · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2605.12863

Language-Based Agent Control

Timothy Zhou, Loris D'Antoni, Nadia Polikarpova

原文摘要

This paper introduces language-based agent control (LBAC), a new programming model for agentic applications that brings techniques from programming languages and language-based security to the problem of agent control. In conventional programming, combinations of static typing and runtime enforcement have long been used to guarantee that well-typed programs satisfy user-specified policies, including policies for access control, information flow, data provenance, and more. The key idea behind LBAC is to extend these guarantees to agentic applications by requiring agents to generate programs that are themselves well-typed in the context of the surrounding scaffolding code. Unsafe programs are rejected by the typechecker before execution, allowing policies to apply uniformly across the entire application, including both agent-generated behavior and developer-written scaffolding. At the same time, LBAC preserves substantial expressiveness: agents may perform arbitrary side-effect-free computation and recursively invoke subagents, which retain full tool access subject to the same--or potentially more restrictive--policies. We demonstrate LBAC with three case studies: I/O sandboxing via filesystem capabilities, data provenance, and information-flow control.

cs.PL · cs.AI · cs.CR

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.10394

Crustify: Repository-Level Generation of Safe Rust Bindings with LLM Agents and Coverage-Guided Testing

Marius Momeu, Marius Arvinte, Cory Cornelius, Koushik Sen

原文摘要

Wrapping C code in a safe Rust interface lets Rust applications use it without writing unsafe code, until the code itself is migrated to Rust. Such bindings are tedious and error-prone to write, however: their internals use unsafe code that the Rust compiler does not check, so a single mistake can introduce undefined behavior (UB), and they have so far been written mostly by hand. We present Crustify, an agentic co-translator that generates safe Rust bindings for repository-level C libraries. Crustify schedules a target's types and symbols into dependency-ordered waves of independent batches that agents bind concurrently. Its agents derive the ownership and lifecycle contract of every pointer and type they wrap, check each binding with coverage-guided equivalence and UB tests under sanitizers and Miri, and review every wave. They build on three tools that we contribute: (a) ffibox, Rust primitives for C/Rust interop that mirror Box, Arc, and Vec for C objects without ever forming a reference to memory that C may alias; (b) Wavefront, a neuro-symbolic static analyzer that orders a target's items by their dependencies, including those that casts and type-erased pointers hide; and (c) ffimap, a rustc-based analysis that maps the unsafe surface of bindings. On libgit2 and ffmpeg, with one developer in the loop, Crustify generated safe bindings for 41.9% and 42.8% of their public APIs in about 51.9 and 58.9 hours. On the interface consumers are expected to use, only 1.6% and 0.4% of the bindings' public functions are unsafe, and only 0.1% and 0.6% have a raw pointer in their signature. Their tests cover 98.92% and 99.07% of the Rust code and 45.95% and 67.20% of libgit2 and of ffmpeg's libavutil, and the reviewers fixed 8 and 13 defects that caused UB reachable from Rust. To our knowledge, this is the first work to automate the generation of safe Rust bindings for C libraries.

cs.PL · cs.AI · cs.CR · cs.SE

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.09846

基于集成的LLM代码摘要无参考置信度估计方法

Ensemble Methodology for Reference-Free Confidence Estimation in LLM-based Code Summarization

Marco Colombo, Balaji A Jayaram, Sowmyakumari Selvaraj, Sumit Tokkar, Animesh Kumar, Aravinda Prasad Sistla, Ravishankar Shetty, Rigel Gjomemo

AI 速读 基于摘要

提出一种无需人工参考摘要、通过多模型语义一致性与LLM评判器聚合来估计LLM生成COBOL摘要正确性的集成方法。

cs.AI · cs.PL

arXiv ↗PDF ↗
查看原文摘要

This paper describes an approach and use case to estimate the correctness of LLM-generated COBOL summaries without access to human-authored references. The core intuition is that inter-model agreement on semantics is informative about truth, and that an LLM-as-judge can provide higher-fidelity pairwise assessments than traditional string- or embedding-based metrics. We operationalise this intuition with (i) controlled summary generation from diverse models; (ii) a LLM evaluator that compares pairs of summaries and emits structured judgments; and (iii) a calibrated aggregation rule that combines supportive evidence while penalising only corroborated contradictions.

版本更新 · v2arXiv:2607.11329

Fuss-free cumulative universes: theory and practice

Raphaël Sterbac, Jonathan Sterling

原文摘要

Universes are central to dependent type theory, and they are notoriously difficult to handle in a way that is both correct and usable. We propose a new "fuss-free" generalised algebraic presentation for polymorphic cumulative universes that dispenses with the intricate theory of coherent universe coercions in favour of a simpler formulation, which we prove equivalent by means of a normalisation theorem for the former. We study the fuss-free formulation by means of (1) an abstract specification of its bidirectional elaboration algorithm, and (2) a concrete implementation in Haskell. We also describe and implement an extension of the fuss-free universe hierarchy with a judgemental notion of datatype description from which prior notions of cumulative inductive type may be derived.

cs.PL · cs.LO · math.LO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.09410

Nothing Is Shared Until You Synchronise: Reinterpreting Java for Data-Race Freedom

Luke Cheeseman, Elias Castegren, David Black-Schaffer, Erik Österlund, Tobias Wrigstad

原文摘要

In mainstream shared-memory languages, programmers use synchronisation mechanisms such as locks to isolate shared data accesses across threads to avoid data races. Yet synchronisation enforces only a temporal ordering, while shared memory still communicates updates between threads at every ordinary read and write. To achieve isolation, programmers therefore need to understand the connection between ordering and communication, and to apply synchronisation correctly and consistently, while compilers and hardware optimise assuming they have. When programmers synchronise incorrectly, they lose isolation, and the semantics of their programs change without notice. We propose Sync-as-Share, a memory model built on isolation and communication rather than on the ordering of accesses to shared memory. We start from thread isolation, where each thread reads and writes a private view of memory, and reinterpret programs' existing synchronisation actions to also communicate updates explicitly. As nothing is communicated outside synchronisation actions, data races become impossible by construction. Instead, conflicting updates are detected at synchronisation points. Viewing synchronisation as explicit communication exposes the design decisions of what should be communicated, to whom, and what counts as a conflict. We propose two communication topologies with different trade-offs. We instantiate Sync-as-Share for Java by making the synchronisation actions already defined by its memory model the only points at which threads communicate, so Java programs can adopt Sync-as-Share unmodified. We formalise this instantiation as version-controlled memory, in which synchronisation actions push and pull updates between private views, and mechanise it in Rocq. We show that Java programs that are correctly synchronised under the Java memory model behave identically under shared memory and Sync-as-Share.

cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v3arXiv:2601.20370

The Program Logic of Abstract Interpretation

Paolo Baldan, Roberto Bruni, Francesco Ranzato, Diletta Rigo

原文摘要

Hoare-style program logics and abstract interpretation are two of the principal frameworks for reasoning about programs, and their affinity has long been recognised informally: both derive over-approximate judgements about program behaviour by structural, syntax-directed reasoning. Turning this analogy into a formal correspondence runs into two challenges. First, the disjunction (or join) rule, sound and admissible in Hoare logic, becomes unsound over non-additive abstract semantics. Second, the extrapolation operators that make abstract interpretation effective on unbounded computations, i.e. widening and narrowing, have no analogue in the derivations of existing program logics. We introduce APPL (Abstract Program Property Logic), a Hoare-style program logic that provides a proof-theoretic foundation for abstract interpretation while addressing both challenges. The key technical idea is density: abstract semantics is additive over dense families of logical assertions. This leads to a density-guarded join rule that enables sound disjunctive reasoning over arbitrary abstract domains. We also internalise the application of widening and narrowing through inference rules for iterative commands. As a result, an entire analysis by abstract interpretation can be viewed as a logical derivation in APPL. The logic is sound over any abstract domain and, when the assertion language is expressive enough, it is also relatively complete. Finally, by interpreting nondeterminism through a monoidal operator, APPL provides a single logical framework that uniformly subsumes Hoare logic, incorrectness logic, and Hoare-style logics for hyperproperties, thereby enabling their abstraction. Remarkably, the density-guarded join rule introduced to handle non-additive abstract semantics is also fundamental in guaranteeing completeness for hyperproperties.

cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2607.15873

A Physically-Realisable Quantum Programming Language with Quantum-Controlled Quantum Channels

Kengo Hirata, Takeshi Tsukada

原文摘要

In contrast to a classical bit, which can only take the value $0$ or $1$, its quantum counterpart---a qubit---can exist in a superposition of $0$ and $1$. This is a superposition of data values, and it is then tempting to superpose programs as well. Indeed, a particular superposition of programs, known as the quantum SWITCH, has attracted considerable attention. A natural way to superpose programs is conditional branching on quantum data, and several studies have pursued this idea. However, there is a well-known semantic difficulty with this approach, and the fundamental question of whether the languages proposed in prior work can be physically realised remains open. This paper proposes a physically realisable quantum programming language with quantum branching over quantum channels. We first analyse the semantic difficulty from an implementation perspective and show that the difficulty is caused by arbitrariness in the implementation. We then design a language that is free from this arbitrariness. As expected from its implementation-oriented design, our language is physically realisable. We argue for this from two directions: first, we give a method for compiling programs into quantum circuits; and second, we show that our programs stay within the physically admissible range, namely, that they neither yield probabilities greater than one nor violate causal inequalities. The absence of such violations is established through the inclusion of our language in QC-QC, a notion of realisability studied in physics.

cs.PL · cs.LO · quant-ph

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.08675

A Complete Calculus for Hamiltonian Quantum Programming

Jacques Carette, Chris Heunen, Robin Kaarsgaard, Neil J. Ross, Amr Sabry

原文摘要

Given the forces acting on a quantum particle, a Hamiltonian models its continuous evolution. Quantum computers evolve Hamiltonians to simulate physical systems, to solve optimisation problems, and to estimate eigenvalues, and even the popular circuit abstraction is compiled to Hamiltonians on the hardware. We introduce Hamilton, a process calculus whose parallel operator is the sum of interactions acting simultaneously. Its operational semantics is the Lie-Trotter product formula, which recovers a sum as the limit of ever finer sequential interleavings; compiling a program means halving it to a chosen precision and unrolling the interleaving into a circuit. The semantics is fully abstract, the expressible Hamiltonians are exactly those whose Pauli coefficients have the form $m/2^k$, the precision that successive halving reaches, and the equational theory is complete and decidable. A full implementation compiles Hamilton programs to circuits and decides their equivalence, and Agda proofs sanity-check the core metatheory.

cs.PL · quant-ph

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.08083

GUARDTs: Decentralized Access Control for Replicated Data Types

Christian Kuessner, Ragnar Mogk, Julian Haas, Annette Bieniusa, Mira Mezini

原文摘要

Replicated data types providing strong eventual consistency offer a principled foundation for developing decentralized software. Yet existing approaches to programming such data types leave access control unresolved: they either provide none at all, delegate it to a trusted coordinator, reintroducing the centralization they were designed to avoid, or tie it to specific data-type constructions, while typically assuming non-Byzantine replicas and static policies. We present GUARDTs: Guarded Unforgeable Algebraic Replicated Data Types, which embed fine-grained permissions directly into the application data model, operate without a central authority, support dynamic policy evolution, and tolerate Byzantine replicas. We formally prove that GUARDTs guarantee confidentiality, integrity, and availability and show empirically that their access control adds negligible overhead on top of the cost of Byzantine-resilient replication itself.

cs.PL · cs.DC

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.07105

NUMA-Torch: Compiler-Driven NUMA-Aware LLM Prefill on Multi-Socket CPUs

Thisara Rathnayaka Weerakoon, Ishan Dewpura, Niman Ransindu, Shavin Anjitha, Tharindu R. Patabandi, Sanath Jayasena

原文摘要

For sufficiently large transformer-based Large Language Models (LLMs), whose parameters cannot be retained in on-chip caches, prefill throughput on multi-socket CPUs is often limited by sustainable DRAM bandwidth rather than peak floating-point throughput. In the standard PyTorch compilation (i.e., TorchInductor) path, model weights are allocated without considering the Non-Uniform Memory Access (NUMA) topology: specifically, the affinity between memory banks and compute cores is disregarded. This causes a substantial fraction of weight accesses to traverse the inter-socket interconnect, severely degrading the effective memory bandwidth available to each socket. We address this bottleneck through a compiler-level solution that makes TorchInductor NUMA-aware. Treating each NUMA socket as an independent tensor-parallel partition, we introduce NUMA-aware Tensor Parallelism (NUMA-TP). This approach transparently shards weights across sockets and schedules compute kernels such that thread pools and memory allocations remain strictly local to their respective sockets using CPU affinity. We evaluate the approach on GPT-2 (117M, 345M, 762M) and BERT (Small, Large), which exercise standard multi-head attention and MLP, as well as Gemma 3 270M, which combines Multi-Query Attention with a GeGLU-gated MLP. By strictly enforcing data locality, our approach successfully mitigates cross-socket traffic, achieving prefill speedups of up to 2.63x on a dual-socket Haswell platform, up to 1.87x on a dual-socket Cascade Lake platform, and up to 2.27x on a four-socket Haswell-EX platform.

cs.DC · cs.PF · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v5arXiv:2505.07681

Verified Purely Functional Catenable Real-Time Deques

Jules Viennot, Arthur Wendling, Armaël Guéneau, François Pottier

原文摘要

We present OCaml and Rocq implementations of Kaplan and Tarjan's purely functional, real-time catenable deques. The correctness of our Rocq code is machine-checked.

cs.PL · cs.DS · cs.LO

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.06319

Verified Implementation of the Next-gen Borrow Checking Algorithm for Rust via Abstract Interpretation

Jinhua Wu, Yuting Wang, Zhemin Chen

原文摘要

Borrow checking is a central mechanism for Rust to ensure temporal memory safety. Its correctness is based on the intuition that the Aliasing XOR Mutability discipline guarantees that programs without borrow errors inherently could not access invalid references (i.e., pointers). However, existing work on formalizing borrow checking treats it either as a component of type systems or as symbolic execution describing resource transfer. None provides a direct explanation of the correctness of borrow checking algorithms such as Non-Lexical Lifetimes (NLL) or Polonius in the official Rust compiler that function more like static pointer analysis. We take a first step toward solving this problem by formalizing Polonius, the next-generation borrow- checking algorithm for the Rust compiler, on a core subset of Rust. We prove its correctness by showing that any program accepted by Polonius does not access invalid references at runtime. The key observation is that, when borrow checking is performed lazily, Polonius could be treated as a forward abstract interpretation on abstract domains recording pointer aliasing (borrowing) relations. By providing a concrete semantics that formally describes the Aliasing XOR Mutability discipline, we prove the soundness of this abstract interpretation, from which we derive memory safety of checked programs. This formulation of Polonius is implemented and formally verified in the abstract interpretation framework of CompCert. The correctness proofs are generated by an agentic AI under human guidance using paper proofs as proof outline. To the best of our knowledge, this is the first comprehensive formalization and verification of a borrow checking algorithm as manifested in the Rust compiler.

cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2403.20132

A formal specification of the jq language

Michael Färber

原文摘要

jq is a widely used tool that provides a programming language to manipulate JSON data. However, the jq language is currently only specified by its implementation, making it difficult to reason about its behaviour. To this end, we provide a formal syntax and denotational semantics for a large subset of the jq language. In particular, we give a translation from jq programs to lambda terms. Our most significant contribution is to provide a new way to interpret updates that allows for more performant execution. We implement our semantics in two interpreters and evaluate the performance.

cs.LO · cs.PL

查看论文
arXiv ↗PDF ↗
版本更新 · v2arXiv:2611.03917

Silent Degradation during Auto-Vectorization of bf16/fp16 on RISC-V Under LLVM

Vaishnavi Kouru, Robert Chun

原文摘要

Low-precision numeric types such as 8-bit integers, bfloat16, and half-precision floating point (fp16) are often used in AI inference workloads to reduce memory bandwidth, and RISC-V's openly specified Vector extension (RVV) is a natural target for compiling such workloads with auto-vectorization. This paper examines whether LLVM's RISC-V auto-vectorizer handles these narrow types equally well, using a multiply-accumulate loop written for fp32, int8, bf16, and fp16. Under a common baseline target (-march=rv64gcv), int8 and fp32 vectorize cleanly, while bf16 and fp16 degrade to increasingly scalar-heavy fallback code, with fp16 falling back to per-element software conversion calls, unless additional target-feature extensions (zvfbfmin/zvfbfwma, zvfhmin) are enabled. Under QEMU user-mode emulation, the baseline bf16 and fp16 kernels execute $17.0\times$ and $75.9\times$ as many dynamic instructions as their extension-enabled counterparts. Compiler diagnostics do report this degradation, but do not distinguish, in their wording, between a limitation that a compiler flag resolves entirely and one reflecting an inherent conversion cost, leaving no direct signal toward the fix. These results are supported by assembly-level instruction analysis, by direct inspection of LLVM's optimization remarks, and by dynamic instruction counts collected under emulation.

cs.PL

查看论文
arXiv ↗PDF ↗
新论文 · v1arXiv:2611.05695

Demystifying Information Flow Downgrading using the Real--Ideal Paradigm

Suraaj Kanniwadi, Andrew C. Myers

原文摘要

The real--ideal paradigm, an approach to security specification developed in the cryptography community, has the benefit that it can express sophisticated confidentiality and integrity requirements, even for decentralized systems. We show that this paradigm is the basis for a powerful and intuitive new semantic framework for language-based security. Our new framework cleanly and extensionally captures existing security definitions, including not only noninterference but also less understood information flow properties that involve downgrading, such as robust declassification and nonmalleable information flow. Past semantics for these properties have relied on intensional downgrading events. Further, we show that all of these properties can be enforced by a practical information-flow type system for a while-language that supports downgrading. Surprisingly, correctness of this type system is also characterized as a real--ideal simulation, with an important implication: the security of heterogeneous, decentralized systems with a strong (real) attacker can be understood by reasoning about a weak (ideal) attacker whose power is restricted to interaction with downgrading. This result explains the usefulness of nonmalleable information flow and related security properties. The results are fully formalized using the Rocq prover and are publicly available.

cs.PL · cs.CR

查看论文
arXiv ↗PDF ↗