pith. sign in

cs.PL

Programming Languages

Covers programming language semantics, language features, programming approaches (such as object-oriented programming, functional programming, logic programming). Also includes material on compilers oriented towards programming languages; other material on compilers may be more appropriate in Architecture (AR). Roughly includes material in ACM Subject Classes D.1 and D.3.

0
cs.SE 2026-07-03

VLP lifts LLM code pass rates from 29-73% to 65-93%

by Ziqi Yuan, Wenhao Lu +3 more

Guiding Human Validation of LLM-Generated Code via Verifiable Literate Programming

Unambiguous natural-language docs let users spot and fix intent mismatches before verification

Figure from the paper full image
abstract click to expand
Vibe coding democratizes software development by allowing users to generate code via natural-language (NL) interaction with large language models (LLMs). However, the code is reliable only when it faithfully implements the user's intent, which is difficult and labor-intensive for users to validate. Existing validation methods either rely on LLM-assisted automated testing, which suffers from prompt ambiguity and model fallibility, or involve users only in partial software artifacts such as prompts and test cases, which may overlook corner cases and program details. Motivated by a bug study of LLM-generated code, we find that detailed human feedback is essential, as failures often stem from underspecified requirements or subtle semantic deviations. This paper presents verifiable literate programming (VLP), a human-in-the-loop framework designed to make the review/validation process of LLM-generated code accessible to users at all programming levels. At its core, VLP proposes unambiguous NL-based documentation as a readable intermediate layer between prompts and code. The documentation demonstrates concrete program semantics and enables users to provide feedback on potential intent-code mismatches. It supports human-involved, end-to-end repair and validation via three techniques: (i) an NL-style literate language with unambiguous syntax and mostly deterministic code-to-documentation translation, (ii) LLM-based fine-grained mismatch detection that uses trace links between prompts and documentation to focus users' review effort on suspicious documentation lines, and (iii) a verification module that leverages user-validated documentation to derive API-usage checks and formal properties, which are then verified against the generated code using model checking. Our evaluation shows that VLP improves code pass@1 from 28.7%-73.2% to 65.4%-93.5% with reasonable user effort.
0
0
cs.SE 2026-07-02

Kani verifies 16000+ Rust harnesses per stdlib change

by Rémi Delmas, Zyad Hassan +10 more

Kani: A Model Checker for Rust

Translates MIR to CBMC to prove functional correctness and absence of panics beyond what the type system guarantees.

Figure from the paper full image
abstract click to expand
Rust's ownership type system prevents memory errors in safe code, but certain desirable properties remain orthogonal to compilation: the soundness of unsafe operations (e.g., raw pointer dereferences), functional correctness, and absence of runtime panics. We present Kani, an open-source model checker for Rust that pushes bounded model checking beyond bug-finding to provide correctness guarantees for these properties. Kani compiles proof harnesses from Rust's Mid-level Intermediate Representation (MIR) into CBMC's bit-precise verification engine, automatically checking a comprehensive set of safety properties with no user annotation. To extend verification from bounded to unbounded, Kani provides a specification language comprising function contracts, loop contracts, quantifiers, and function stubbing. We demonstrate feasibility through case studies on industrial Rust projects, where contracts upgraded verification from panic-freedom to functional correctness, uncovering six previously unknown bugs. Kani operates at scale in production CI, with over 16,000 harnesses verified per code change in the Rust standard library verification campaign.
0
0
cs.PL 2026-07-02

Bisimulation proof equates Copilot monitors with compiled code

by Ryan G. Scott, Ivan Perez +3 more

Trustworthy Runtime Verification via Bisimulation (Extended Experience Report)

Generated proofs confirm matching outputs and crash behavior for each monitor using symbolic execution of LLVM.

Figure from the paper full image
abstract click to expand
When runtime verification is used to monitor safety-critical systems, it is essential that monitoring code behaves correctly. The Copilot runtime verification framework pursues this goal by automatically generating C monitor programs from a high-level DSL embedded in Haskell. In safety-critical domains, every piece of deployed code must be accompanied by an assurance argument that is convincing to human auditors. However, it is difficult for auditors to determine with confidence that a compiled monitor cannot crash and implements the behavior required by the Copilot semantics. In this paper we describe CopilotVerifier, which runs alongside the Copilot compiler, generating a proof of correctness for the compiled output. The proof establishes that a given Copilot monitor and its compiled form produce equivalent outputs on equivalent inputs, and that they either crash in identical circumstances or cannot crash. The proof takes the form of a bisimulation broken down into a set of verification conditions. We leverage two pieces of SMT-backed technology: the Crucible symbolic execution library for LLVM and the What4 solver interface library. Our results demonstrate that dramatically increased compiler assurance can be achieved at moderate cost by building on existing tools. This paves the way to our ultimate goal of generating formal assurance arguments that are convincing to human auditors.
0
0
cs.PL 2026-07-02

Inference slashes annotations for range refinement types

by Valentin Aebi, Carlo A. Furia

Practical Range Refinement Types with Inference

Ranger verifies index safety in loops and arrays using bidirectional typing plus flow analysis and needs fewer annotations than prior tools.

Figure from the paper full image
abstract click to expand
Refinement types are a static verification technique that aims at increasing the expressivity of traditional type systems while remaining easy and natural to use. While systems based on refinement types have been developed for several mainstream languages, their practical adoption remains limited by their annotation overhead, which is often a more significant burden than when using the "plain" type annotations of languages like Java or Scala. To improve the state of the art, this paper introduces Ranger: a refinement type system designed to keep the annotation overhead small and to seamlessly integrate with imperative-style constructs like variables and loops. As the name suggests, Ranger focuses on integer range types: a particular kind of refinement types that express bounded integer ranges. Such types are widely useful to verify correct index manipulation and in-bounds data accesses, among others. To combine expressiveness and succinctness, Ranger is based on a bidirectional type system, which runs a type inference algorithm to provide the typechecking pass with information useful to reduce the need for user-written auxiliary annotations. Ranger also integrates other forms of lightweight flow-sensitive static analysis techniques that precisely capture the program's behavior without explicit annotations. We implemented Ranger on top of the Licorne experimental programming language. Our experiments show that Ranger's implementation can concisely express and verify a variety of useful properties that fall beyond the capabilities of standard static type systems like those of Java and Scala, and that Ranger compares favorably to other extended type systems, such as the Java Checker Framework and Liquid Java, that can also check properties about ranges.
0
0
cs.SE 2026-07-02

Ensemble of LLMs fixes up to 22% of LLVM compiler issues

by Zhao Tian, Yingquan Zhao +3 more

LLVM-Bench: Benchmarking and Advancing Large Language Models for LLVM Compiler Issue Resolution

New benchmark of 423 real tasks shows single models lag on patches and builds but combining outputs raises success

Figure from the paper full image
abstract click to expand
LLVM is a widely used compiler infrastructure whose scale and complexity make issue resolution labor-intensive and challenging. Although large language models (LLMs) have recently achieved remarkable success in issue resolution, their effectiveness on complex system-level LLVM compiler remains largely unexplored. To address this gap, we introduce LLVM-Bench, the first large-scale benchmark for LLVM issue resolution, containing 423 real-world, validated tasks collected from the LLVM project. We further develop LLVM-Gym, a scalable evaluation platform that automates issue reproduction, patch application, compiler building, and test execution. Using LLVM-Bench and LLVM-Gym, we conduct a comprehensive study of four representative LLMs, six retrieval configurations, and three agents. Our results show that current LLM-based issue resolution techniques remain limited on LLVM-Bench, with patch invalidity and build failures as the dominant failure modes. We further reveal a strong complementarity among different LLMs and agents, motivating LLVM-Ens, a lightweight ensemble approach that expands the patch space through integrating the patches generated by diverse techniques, filters incorrect and redundant candidates, and identifies the most promising solution. Our results show that LLVM-Ens achieves a resolution rate of up to 21.99%, further improving LLVM issue resolution.
0
0
cs.PL 2026-07-02

Trusted checker blocks optimizer bugs from accepting unsafe rewrites

by Yuan Si, Jialu Zhang

Certificate-Carrying Transformation of Event-Driven Block Programs

For Scratch programs, recomputing every side condition ensures behavior preservation even if the optimizer is buggy.

Figure from the paper full image
abstract click to expand
Block-based end-user languages such as Scratch run tens of millions of programs. Existing tools establish behavior preservation through program analysis and testing without a checked guarantee. We turn optimization into certificate-carrying source-to-source rewriting. An untrusted optimizer proposes a rewrite; a trusted, fail-closed checker accepts it only after recomputing every side condition that the rewrite's behavior preservation depends on under an explicit observation lens. The checker is the sole authority: given a correct checker and a small, explicitly stated set of model-to-VM assumptions, an optimizer bug cannot mint an unsound acceptance. The observation lens is a parameter, and the central soundness argument is a cooperative-frame refinement theorem: a write overwritten before any thread observes it, within a window in which no thread yields, can be removed. We mechanize this theorem in Lean and show that one parametric statement covers two concrete rewrite families instantiated to variable state and renderer state. We build a checker for six rewrite families and evaluate it on 300 real Scratch projects. The checker accepts a behavior-preserving rewrite on 94.3% of projects (283 of 300); certification costs under one tenth of a second per project; and a cross-family adversarial campaign of 4,278 perturbed rewrites produces zero false accepts. An audit found eight false accepts the per-family test suites missed; each is now rejected. An ablation that strips the semantic side conditions, leaving analysis and testing alone, ships rewrites the virtual machine confirms change behavior; the full checker rejects every one. The result shows how to provide behavior-preservation guarantees for a concurrent, event-driven, end-user language. The checker recomputes every required condition instead of trusting optimizer claims, keeping the trusted base small.
0
0
cs.LG 2026-07-02

Targeted edits flip PBE programs that random typos miss

by Yuan Si, Jialu Zhang

Fixed-Set Robustness in Programming by Example: Example Corruption and Semantic Partition Recovery

Semantic partition recovery works only when clean semantics already carry a decisive vote margin, which is rare on standard benchmarks.

Figure from the paper full image
abstract click to expand
Programming-by-example systems infer programs from a small set of input-output examples. Robust PBE work usually models wrong examples as samples from a stochastic noise process and then minimizes an expected or empirical loss. This paper studies a different failure mode: an adversary who sees the synthesizer and chooses the examples whose corruption most damages the returned program. We formalize fixed-set worst-case corruption for finite PBE version spaces, implement exact-within-bounded-pool and heuristic corruption searches for a string-transformation DSL, and introduce version-space partition aggregation (VPA), a defense that synthesizes on disjoint example groups and votes by semantic signatures. The central claim is deliberately bounded and partly negative: low-margin PBE tasks have an adversarial robustness dimension that random-typo and noisy-PBE evaluations miss, while semantic partition aggregation helps only when the clean semantics keep a partition vote margin, which often fails on realistic tasks. Evidence from curated/generated DSL tasks, accepted public SyGuS PBE_SLIA slices, SYNTRA Playgol v2, and noisy-PBE objective baselines supports that boundary. One curated edit flips all 8 spike tasks while 200-trial typo, DSL-pool, and distance-matched random controls succeed on 10.3%, 11.0%, and 16.7%; generated margin-1 rows flip under budget 1 yet VPA recovers them; on public SyGuS the vote margin is near one, so an adaptive attacker drives VPA accuracy to zero; accepted public SyGuS slices move across exact-within-pool budget boundaries; and Playgol shows positive paired-bootstrap gaps against typo and same-pool random controls on the 141 accepted rows. A small exact-output prompt harness over 20 controlled margin-1 tasks shows the same qualitative clean-to-attacked pattern across local and API models, while it is treated as a scope check, not a broad LLM benchmark.
0
0
cs.SE 2026-07-01

Benchmark shows LLMs reuse old algorithms on shifted problems

by Xinyuan Song, Zekun Cai +1 more

AlgoBench: Benchmarking Algorithmic Adaptation in Code Generation

AlgoBench transforms competitive programming tasks so original solutions fail, exposing limits in algorithmic adaptation.

Figure from the paper full image
abstract click to expand
High pass rates on established programming benchmarks such as HumanEval and LiveCodeBench do not always show whether a model can reason about algorithms. Many fixed benchmarks eventually become part of the public training ecosystem through released problem statements, editorials, and generated solutions, allowing later models to improve partly by exposure rather than by stronger algorithmic ability. We introduce ALGOBENCH, a framework that automatically builds novel algorithmic problems from known competitive-programming problems through structured constraint-shifting transformations. Each accepted ALGOBENCH variant is traceable to a source problem, but must make the original reference algorithm fail. Beyond pass@$k$, we introduce complexity-aware metrics -- including OPTT, OPTS, TRAPRATE, GAPT, and CONSENS -- to test whether a solution is not only functionally correct but also asymptotically suitable for the generated problem. Experiments across multiple LLMs and prompting strategies show that performance drops sharply on ALGOBENCH variants, retrieval can increase reuse of the old algorithm, and many correct-looking solutions fail to meet the required complexity. Error analysis shows that failures are mainly algorithmic rather than implementation-level, suggesting that ALGOBENCH evaluates adaptation beyond functional correctness.
0
0
cs.SE 2026-07-01

LLVM -O3 pipeline regresses in 6.6-9.7% of pass steps

by Federico Bruzzone, Walter Cazzola

A Multi-Dimensional, Per-Pass Empirical Study of the LLVM Optimization Pipeline

Per-prefix measurements on 30 kernels show most gains arrive late and the final config loses on size-speedup for 29 kernels.

Figure from the paper full image
abstract click to expand
Quantifying the marginal impact of individual optimization passes underpins phase ordering, pass selection, optimization design, and analysis of pass/hardware interactions. In LLVM -- the standard backend for C/C++, Rust, and ML stacks via MLIR -- interactions among optimization passes, measurement noise, and pipeline scale make this difficult. We present a systematic, empirical study of the LLVM -O3 optimization pipeline. We decompose the pipeline into cumulative per-pass prefixes. We then measure execution time, compile time, binary size, hardware counters, and RAPL energy across 84,750 measurements covering 113 cumulative prefixes of the -O3 pipeline evaluated on 30 PolyBench/C kernels under rigorous noise mitigation. On these compute-bound affine kernels, the pipeline is non-monotone (6.6-9.7% of transitions regress) and strongly back-loaded (the median non-regressing kernel needs 84.8% of the pipeline for 80% of its speedup). Most gains are driven by a small Pareto-dominant core of passes, while the final -O3 configuration is Pareto-dominated on (size, speedup) for 29 of 30 kernels. We further show that IR instruction count is an unreliable predictor of runtime, that runtime-targeted passes are de facto energy-targeted (30-60% savings), and that the search-free idealized-additive upper bound on losses due to phase interference is 46.35%. These findings enable more informed pass pruning, cost-model calibration, and autotuning.
0
0
cs.CC 2026-06-30

Access cost grows as fourth root of data size

by Chen Ding

The Fourth-Root Complexity of Data Movement

Abstract memory hierarchy shows per-access costs scale as N to the 1/4 for common apps, distinguishing power-law from exponential miss ratio

abstract click to expand
Time complexity typically assumes $O(1)$ cost per data access. This paper presents an analysis based on an abstract memory hierarchy. For a common class of applications, it shows that the data-access cost scales with the fourth root of data size, that is, as data size $N$ increases, the cost of each access increases at the rate of $N^\frac{1}{4}$. While the analysis does not predict performance, it predicts scalability. Specifically, the paper provides a precise analysis that shows the constant-factor difference between cases where the miss ratio follows a power law versus an exponential decay.
0
0
cs.PL 2026-06-30

Well-typed staged code is contextually equivalent to its unstaged erasure

by Jun Tan, Guannan Wei

When Do Staging Annotations Preserve Semantics? Mechanizing Typed Semantics-Preserving Multi-Stage Programming with Let-Insertion (Extended Version)

Binary logical relations prove preservation once let-insertion is tracked as a control effect in two-stage calculi.

Figure from the paper full image
abstract click to expand
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, $\lambda_{|2|}$ and $\lambda^{ref}_{|2|}$, 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 $t_1$ evaluates to a value $\mathsf{code} t_2$, then $t_2$ is contextually equivalent to the stage-erasure of $t_1$. 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.
0
0
cs.PL 2026-06-30

Normal-form search yields 8.93x faster program synthesis

by Zoey Shepherd (1), Ohad Kammar (1) +3 more

NSynC: Normalised Synthesis of Computation

Enumerating semantics directly avoids evaluating duplicate programs that differ only in syntax.

Figure from the paper full image
abstract click to expand
Inductive program synthesis algorithms search a space of programs to find one that meets some specification. Enumerating according to the syntax of a programming language leads to a large search space, and hence slow synthesis, due in large part to semantic duplication. A synthesiser may have to evaluate -- and reject -- multiple semantically identical but syntactically different programs, wasting resources. To avoid this duplication, we present NSynC, a synthesis-by-semantics approach. By enumerating the semantics of the target language directly, we guarantee that each candidate program is semantically unique and that each evaluation of a candidate is meaningful. Specifically, we search the space of normal forms for the simply-typed lambda calculus with sums using a top-down, type-directed synthesis algorithm. Our preliminary results show a geomean speedup of 8.93x on a synthetic benchmark suite over the unrestricted algorithm.
0
0
cs.PL 2026-06-30

Dynamic graphs let MCMC skip unchanged computations

by Viktor Palmkvist, Fredrik Ronquist +1 more

Reactive Graphs for Efficient Markov Chain Monte Carlo Inference in Probabilistic Programming Languages

By representing data dependencies explicitly, proposals update only the relevant subgraph, increasing samples per unit time.

Figure from the paper full image
abstract click to expand
An important aspect of making inference based on a probabilistic program practical is efficiency; faster evaluation enables more work per unit of time, which can be translated into more precision. Inference via Markov chain Monte Carlo has a property that can be favorably exploited for efficiency: most proposed samples are computed as minor variations of previous samples, i.e., a clever implementation can skip computations pertaining to what is unchanged. This paper provides an approach for automatically translating a probabilistic program to a dynamic graph, reminiscent of functional reactive programming, that explicitly represents data dependencies, enabling proposals to only recompute the parts of the graph that depend on redrawn random variables. The graph-building interface follows familiar functional programming interfaces, which also connect to their expressiveness in terms of probabilistic programming: models using the applicative functor portion express Bayesian networks, while those using monads represent universal probabilistic programming languages.
0
0
cs.PL 2026-06-29

Langshaw declares protocols with sayso priority and conflict rules

by Munindar P. Singh, Samuel H. Christie V +1 more

Langshaw: Declarative Interaction Protocols Based on Sayso and Conflict

Sayso assigns attribute control while nono and nogo handle action conflicts for flexible multiagent enactment.

Figure from the paper full image
abstract click to expand
Current languages for specifying multiagent protocols either over-constrain protocol enactments or complicate capturing their meanings. We propose Langshaw, a declarative protocol language based on (1) sayso, a new construct that captures who has priority over setting each attribute, and (2) nono and nogo, two constructs to capture conflicts between actions. Langshaw combines flexibility with an information model to express meaning. We give a formal semantics for Langshaw, procedures for determining the safety and liveness of a protocol, and a method to generate a message-oriented protocol (embedding needed coordination) suitable for flexible asynchronous enactment.
0
0
cs.CR 2026-06-29

Learned transformations raise symbolic execution coverage 3.69x

by Jie Zhu, Penghui Li +5 more

Symbolon: Symbolic Execution by Learning Code Transformation

Distilling search results from small programs into agent skills cuts memory and solver time while exposing new kernel bugs.

Figure from the paper full image
abstract click to expand
Symbolic execution is a powerful program analysis technique with broad applications, such as vulnerability detection, security testing, and malware analysis. However, this technique is known to suffer from scalability issues, e.g., path explosion, complex constraints, due to certain structural and semantic patterns commonly presented in real-world programs. Existing approaches attempt to escape these patterns by transforming programs into new representations to reduce the execution cost. Unfortunately, these transformations are often too rigid to exploit diverse local program semantics and sometimes rely on compiler optimizations designed for concrete execution that may misalign with the goals of symbolic execution. We present Symbolon, a framework that automatically learns diverse code transformations and applies them context-sensitively to improve symbolic execution. Our key insight is to formulate transformation discovery as a search problem over program representations. To make the search practical, Symbolon learns transformations cheaply offline on small programs, distills them into a reusable library of agent skills, and uses an agent to instantiate these skills on repo-level targets. Our evaluation shows that Symbolon substantially improves the symbolic execution engine KLEE across 16 search strategies on 32 real-world programs, increasing line coverage by 3.69x on average while reducing peak memory and per-query solver time by 29.2x and 123x, respectively. When applied to the latest Linux kernel, Symbolon uncovers 21 previously unknown bugs, all of which have been reported to the kernel maintainers.
0
0
cs.LO 2026-06-29

KoAT infers runtime bounds for integer programs automatically

by Nils Lommen, Éléanore Meyer +1 more

KoAT: Automatic Complexity and Termination Analysis of Integer Programs

Modular analysis of subprograms with multiple techniques yields termination proofs and complexity results for recursive code.

Figure from the paper full image
abstract click to expand
KoAT is a tool to automatically infer complexity bounds and prove termination of (possibly recursive) integer programs. To this end, KoAT implements an alternating modular inference of upper runtime and size bounds for program parts. In particular, KoAT uses a portfolio of different techniques to analyze subprograms. The power of our approach is demonstrated by an extensive experimental evaluation.
0
0
cs.PL 2026-06-29

Prophecy lists reduce message-passing checks to CHC satisfiability

by Takashi Nagatomi, Musashi Katsura +3 more

Prophecy-Based Automated Verification of Message-Passing Programs

Future-value lists plus timestamps let sender and receiver threads be encoded separately while preserving exact correctness.

Figure from the paper full image
abstract click to expand
We propose a fully automated method for verifying functional correctness of message-passing concurrent programs by reducing verification problems to constrained Horn clause (CHC) solving. Inspired by RustHorn's prophecy-based technique, we represent each sender channel by a list of values to be sent over the channel in the future, which enables modular encoding of sender and receiver threads in CHCs. To capture causal dependencies between different channels, we further attach timestamps to messages. We prove that the resulting reduction is sound and complete: a program is free from assertion failures if and only if the corresponding system of CHCs is satisfiable. We have also implemented a prototype verifier for Rust-like programs and experimentally confirmed the effectiveness of the approach.
0
0
cs.PL 2026-06-29

Translations equate two styles of graded coeffect calculi

by Vilem Liepelt, Danielle Marshall +1 more

Same Coeffect, Different Base: Connecting Two Dominant Approaches to Graded Types

Graded-base and linear-base systems model the same context dependencies via type-grade-semantics preserving mappings.

Figure from the paper full image
abstract click to expand
Graded types provide a way to augment a type system with fine-grained information, e.g., to track side effects or context dependence and resource use (called coeffects). Graded types for coeffects have found their way into languages such as Haskell, Idris, and Granule, enabling resourceful reasoning via coeffect analysis with varying levels of generality. Two separate lineages of graded coeffect system have emerged in the last decade: those in which coeffect annotations are pervasive, requiring annotations on function types (which we call graded-base) and those in which coeffects are added by way of a graded modal type operator atop linear types (which we call linear-base). The latter has its origins in Girard's Linear Logic which has been a rich humus for programming language research focused on resources, whereas the graded-base approach emerged in the mid-2010s, seeing rapid adoption in programming language theory and practice, e.g. in QTT and Linear Haskell. The relationship between these two styles has however remained an open question. We answer this question by giving translations between pairs of calculi of both lineages that we prove type-, grade- and operational-semantics preserving. We show that the same notions of context dependence can be expressed in either style, building a bridge between the two lineages that enables transfer of results and ideas, while helping language designers to make better informed choices.
0
0
cs.LO 2026-06-29

Quantum instrument monad generalizes state monad to quantum systems

by Tobias Fritz

The quantum instrument monad

It models computation-quantum interactions via a new integral on type I algebras and is shown to be a strong monad in both finitary and meas

abstract click to expand
Monads are a ubiquitous structure in functional programming used for modelling computational effects. For example, the state monad models the effect of a computation interacting with a memory system. Here we introduce the quantum instrument monad $\mathcal{I}_\mathcal{A}$, which models the effect of a computation interacting with a quantum system with algebra of observables $\mathcal{A}$. It can be thought of as a noncommutative generalization of the state monad. We construct this quantum instrument monad in two versions: a finitary version on the category of sets and a measure-theoretic version on the category of measurable spaces (the latter under the assumption that $\mathcal{A}$ is a type I von Neumann algebra with separable predual). Both versions are strong monads. The construction of the measure-theoretic version is based on a new notion of integral of a quantum-operation-valued function against a state-valued measure.
0
0
cs.SE 2026-06-26

Object orientation creates the fragmentation it seeks to avoid

by Daniel Jackson

Beyond Objects

The principle of tying functionality to domain objects leads to inevitable problems that later methods cannot fix.

Figure from the paper full image
abstract click to expand
A core principle of object orientation -- that the functionality of a system can be partitioned amongst objects that correspond to individuals in the problem domain -- has influenced how software has been specified, designed and implemented for more than fifty years. Later developments in software engineering sought to build on this principle. But in fact this partitioning is neither natural nor straightforward, and the problems that these later developments sought to mitigate -- the fragmentation and conflation of functionality -- were often, in fact, the inevitable consequences of this founding principle. An easier path to addressing these problems therefore starts by going back, abandoning object orientation, and replacing it with an alternative approach that decouples the individuals of the problem domain from the modules that partition functionality.
0
0
cs.PL 2026-06-26

Runtime adaptors implement Go generics with structural subtyping

by Raymond Hu, Julien Lange +4 more

Welterweight Go: Boxing, Structural Subtyping, and Generics (Extended Version)

Type-directed compilation to a runtime model preserves separate compilation and avoids code generation.

Figure from the paper full image
abstract click to expand
Go's unique combination of structural subtyping between generics and types with non-uniform runtime representations presents significant challenges for formalising the language. We introduce WG (Welterweight Go), a core model of Go that captures key features excluded by prior work, including underlying types, type unions and type sets, and proposed new features, such as generic methods. We also develop LWG, a lower-level language that models Go's runtime mechanisms, notably the distinction between raw struct values and interface values that carry runtime type information (RTTI). We give a type-directed compilation from WG to LWG that demonstrates how the proposed features can be implemented while observing important design and implementation goals for Go: compatibility with separate compilation, and no runtime code generation. Unlike existing approaches based on static monomorphisation, our compilation strategy uses runtime type conversions and adaptor methods to handle the complex interactions between structural subtyping, generics, and Go's runtime infrastructure.
0
0
cs.PL 2026-06-26

Reboot converts C interpreters to safe Rust with 1-11 fixes

by Bo Wang, Brandon Paulsen +4 more

Mostly Automatic Translation of Language Interpreters from C to Safe Rust

Six programs pass all original tests and most validation tests while losing their memory bugs.

Figure from the paper full image
abstract click to expand
Translating C programs to safe Rust is challenging owing to significant differences in typing constraints, ownership, and borrowing rules. Interpreter programs are particularly important targets for such translation, as they often handle untrusted inputs and suffer from memory-related vulnerabilities. We present Reboot, a mostly-automatic technique that translates real-world interpreter programs from C to safe Rust. Using Reboot, we have translated six interpreters ranging from 6k to 23k lines of C code to safe Rust, with each translation requiring only 1 to 11 brief user interventions. All translations pass 100% of the provided test suites, and achieve 62%--92% pass rates on separately created validation tests that were never exposed to the system. A security case study on mujs shows that memory vulnerabilities such as heap buffer overflows and use-after-free present in C are eliminated in the safe Rust translation. Two ideas underpin Reboot. First, feature reduction decomposes the translation by program features, creating a sequence of milestones where each is a complete, testable program; the translation starts from the simplest version and incrementally restores features, with each milestone validated before proceeding. Second, a multi-agent architecture orchestrates inherently unreliable coding agents through automated validation and feedback, keeping long-running translation workflows on track with minimal human involvement. An ablation study confirms that feature reduction improves translation correctness compared to using multi-agent translation alone, with 6%--20% improvements in pass rates on validation test suites.
0
0
cs.LO 2026-06-26

Lean formalizes many-sorted modal logic with soundness proof

by Andrei-Alexandru Oltean, Bogdan Macovei +1 more

Formalizing a Many-Sorted Hybrid Polyadic Modal Logic in Lean

The formalization includes a soundness proof and a DSL to define and check programs and security protocols without extra syntax.

abstract click to expand
We present a Lean formalization of a general hybrid modal logic with many-sorted signatures and polyadic modal operators. The system borrows ideas from both algebraic specification and dynamic logics, and is designed to serve as a uniform axiomatic foundation for specifying and verifying programming languages and security protocols. We expose a DSL for users to define languages and protocols as many-sorted signatures, specify the relevant domain-specific axioms, and reason about program executions or protocol runs. We provide a machine-checked proof of its soundness theorem and showcase the framework's versatility through several applications: an imperative programming language for code verification, the BAN logic for security protocols, and the modal system S5. We have designed our formalization to be intrinsically sorted, that is, well-sorted formulas in the base language are well-typed terms in Lean. Thanks to intrinsic sorting, all domain specific applications can be easily embedded in our framework via the DSL, at no additional syntactic overhead required for the user to prove. All code presented in this paper is openly accessible in the following repository: https://github.com/alexoltean61/msphml-lean
0
0
cs.PL 2026-06-26

Compiler automates approximation tuning for hyperdimensional computing

by Xavier Routh, Abdul Rafae Noor +5 more

Compiler-Driven Approximation Tuning for Hyperdimensional Computing

ApproxHDC searches the space of possible approximations to deliver performance gains on CPUs, GPUs, and memory accelerators with little accu

Figure from the paper full image
abstract click to expand
As Moore's law reaches its physical and economic limits, domain-specific approaches are increasingly employed to accelerate machine learning workloads. Hyperdimensional Computing (HDC) represents one such emerging paradigm, offering an alternative to conventional deep learning techniques. Rooted in cognitive models of computation, HDC is designed bottom-up with hardware efficiency as a first-class objective. HDC workloads map naturally to heterogeneous hardware platforms, including CPUs, GPUs, and FPGAs, as well as emerging in-memory computing technologies such as Resistive RAM (ReRAM) and Phase-Change Memory (PCM). HDC algorithms are intrinsically tolerant to noise and approximation, enabling substantial performance gains with minimal accuracy loss. In this work, we introduce ApproxHDC, a framework for automated identification and application of domain-specific approximations in HDC workloads. ApproxHDC extends the HPVM-HDC compiler infrastructure to enable retargetable compilation across diverse hardware backends, including CPUs, GPUs, and simulated ReRAM and PCM-based accelerators. The space of possible approximations is exponentially large; ApproxHDC employs efficient search and analysis to navigate it and identify high-impact configurations spanning both software and hardware levels.
0
0
cs.LG 2026-06-26

Benchmark shows AI formalizes only 20% of logic textbook

by Yuming Feng, Frederick Pu +6 more

Theory-Scale Auto-Formalization of Logics for Computer Science

Dataset of 327 interdependent items and 85K lines of Lean code tests coherent translation of definitions and theorems.

Figure from the paper full image
abstract click to expand
Auto-formalization is critical for scalable formal verification, but existing progress largely focuses on isolated statements, while theory-scale auto-formalization, which coherently translates hundreds of interdependent definitions, lemmas, and theorems, remains open due to challenges in consistency, faithfulness, scalability, and correctness. In this paper, we introduce LCS-Bench, a stand-alone, theory-scale benchmark based on Logics for Computer Science. LCS-Bench is built through a novel semi-automated agentic pipeline that leverages concept graphs, formal signature planning, issue tracking, sorry-filling with counter-example search, complemented by faithfulness review from human experts. The resulting artifact covers 327 textbook items, over 4,076 Lean declarations, and more than 85K lines of Lean code. The dataset supports broad evaluation through a data engine that automatically derives five tracks of evaluation benchmarks, measuring different aspects of auto-formalization and theorem-proving capabilities. We also introduce a novel evaluation protocol featuring definitional equivalence checkers, enabling more fine-grained and faithful assessment. Through extensive evaluation on 14 models, we demonstrate that (1) LCS-Bench is of high quality, consistent, and faithful; (2) the benchmark is challenging, with state-of-the-art models achieving only 20.1% on auto-formalization tasks; and (3) our analysis reveals key findings regarding theory-scale auto-formalization and suggests promising directions for future work.
0
0
cs.SE 2026-06-26

LLMs preserve VeriFast spec behavior at 91% but verify at 31%

by Wen Fan, Minh Tran +6 more

An Empirical Study of LLM-Generated Specifications for VeriFast

Empirical test on 303 C functions shows errors mostly come from missing separation logic knowledge.

Figure from the paper full image
abstract click to expand
Static verification tools can assure industrial scale software, but require significant human labor to write specifications. This is particularly true of static verifiers based on separation logic (SL verifiers), which excel at verifying heapmanipulating programs, but require many complex auxiliary specifications to reason about heap structure. Recent work applies large language models (LLMs) to generate code, tests, and proofs, including specifications for verifiers, but mostly targeting non-SL verifiers. To address this gap, this paper thoroughly evaluates how well LLMs perform when prompted to generate specifications for verifying 303 C functions with the SL verifier VeriFast. We explored eight prompting approaches, ten LLMs, and three input types in two stages. Quantitative and qualitative analyses are used to assess the LLM-generated code and specifications for functional behavior, verifiability and errors. The results show that LLMs preserve functional behavior in source code and specifications (both over 91%), but achieve modest verification success (31.4%). Using Gemini 2.5 Pro and providing formal contracts lead to higher success rates in our setting. Moreover, most errors (94%) come from LLMs' mistakes in the domainspecific knowledge of SL verifiers such as VeriFast. These findings provide guidance for optimizing LLM-generated specifications for SL verifiers.
0
0
cs.PL 2026-06-25

Typestate tracks purpose sets to enforce data compliance at compile time

by Joan Montas (1), Samuel Dodson (1) +2 more

A Typestate Approach to Purpose-aware Programming

PurPL represents allowed uses as type states that grow or shrink, enabling static checks on sensitive data handling in object-oriented code.

Figure from the paper full image
abstract click to expand
Real-world applications often require verification that sensitive data is being used for their intended purpose. However, existing literature offers limited results regarding compile-time guarantees in this domain. In this paper, we explore the use of typestate to reason about the purpose of data. In typestate, types have a state, which can transition to other states in the style of automata. In our approach, the state of the type of sensitive data is defined as the set of purposes for which the data can be used. This set can grow or shrink at runtime as purposes can be added or removed during execution. In this paper, we have developed PurPL, an object-oriented programming language that features a typestate system that is capable of reasoning about purposes and data usage compliance according to them. We give an overview of PurPL through examples and present a formal type system. We have also implemented PurPL's type checker, and we report on our experiments with type checking various programming scenarios that handle sensitive data.
0
0
cs.PL 2026-06-25

SMT verifies tensor transformations without rewrite rules

by Akash Kothari, Shaowei Zhu +2 more

Axon: A Synthesizing Superoptimizer for Tensor Programs

Axon synthesizes kernels for AI accelerators by propagating operators and checking equivalence over unbounded tensor domains.

Figure from the paper full image
abstract click to expand
Writing high performance kernels for AI accelerators requires deep expertise in tiling, instruction selection, data layout, and operator fusion placing a significant burden on programmers. In this paper, we focus on tile based AI accelerator programs and present Axon, a synthesizing superoptimizer for tensor programs: it uses program synthesis to automatically generate target instructions from semantics specifications, and explores semantically equivalent program variants to select the best performing kernel empirically. Axon discovers algebraic transformations by propagating operators through computation graphs and uses SMT over unbounded tensors to guarantee that all transformations preserve semantics without requiring hand crafted rewrite rules. It then lowers tensor operations to target ISA instructions, explores tiling configurations constrained by hardware descriptions, and fuses operators and instructions to minimize memory traffic.
0
0
quant-ph 2026-06-25

Framework classifies quantum languages and spots design challenges

by Quan Do, Hersh Gupta +6 more

A Survey of Quantum Programming Languages

By comparing ten popular languages, the survey pinpoints issues future quantum programming tools must solve to match classical ones.

Figure from the paper full image
abstract click to expand
Quantum computing has seen multiple recent breakthroughs and is getting closer to demonstrations of an exponential advantage over classical computing for certain problems. Programmers will require high-level, general-purpose, executable programming languages to express quantum solutions clearly and effectively, and the field has already produced a wide variety of such languages. This paper presents a language classification framework and uses it to survey ten popular quantum programming languages. The findings include conceptual and experimental comparisons that result in a list of challenges for future language design.
0
0
cs.LO 2026-06-25

Reordering freedom secures info flow for persistent memory

by Graeme Smith

Information flow security on persistent memory

The condition used for x86 out-of-order execution extends to crash-resilient memory propagation rules.

abstract click to expand
Persistent memory is a recently proposed memory paradigm that delivers many system-wide benefits, including improved runtime efficiency and the ability of programs to recover from power outages and system crashes. While recent research has investigated techniques for proving functional correctness of programs running on related architectures, this is not the case for the orthogonal concept of information flow security. In this paper, we provide an information flow logic for an unstructured language (i.e., with gotos rather than loops) modelling a simple assembly language. We apply this logic to x86 assembly using a notion of reordering interference freedom (rif) to reason about potential out-of-order propagation of instructions to memory. We then show how this same notion of rif can be used to similarly reason about information flow on persistent memory.
0
0
cs.PL 2026-06-25

MLIR abstractions align with term-rewriting and refinement theories

by Javed Absar

Reading AI Model Compilation in MLIR Through the Lens of Formal Theories

Formal correspondences clarify completeness and trade-offs as coding agents handle more implementation.

Figure from the paper full image
abstract click to expand
Compiler infrastructures such as MLIR rest on a set of design principles: IR abstractions, interfaces, match-and-rewrite, flow analysis, type conversion, staged lowering, and so on. These concepts have proven themselves in practice. Good designs typically arrive through engineering knowledge, intuition and experience. Many of them, however, have correspondences in formal theory. MLIR's match-and-rewrite engine has correspondence to a \emph{term-rewriting-system}~\cite{baadernipkow1998}; staged lowering has the structure of \emph{refinement calculus}~\cite{back1998}; and range analysis is grounded in \emph{abstract interpretation}~\cite{cousot1977,cousot1979}. Highlighting these correspondences is useful because each theory supplies vocabulary precise enough to discuss structural questions. Moreover, as coding agents lower the cost of implementation, good design and abstractions become the main concern~\cite{Lattner2026ClaudeCCompiler}. A coding agent can generate a pass, but it can only reason over the semantics the representation exposes. When essential structure is missing, the limitation is one of abstraction, not of implementation. The natural next question is how to design that substrate well. Well-chosen abstractions emerge from experience and intuition, but they often mirror concepts given a more precise treatment in formal theory. We argue that knowledge of these formal concepts clarifies what completeness means for a given abstraction, what the ideal design would be, and where practical trade-offs depart from it.
0
0
cs.LO 2026-06-24

Relaxed NFL turns informal math into verifiable formal proofs

by Zhicheng Hui, Lihan Xie +4 more

Verifiable Auto-Formalization of Mathematics Using a Relaxed Natural Formal Language

It keeps human reasoning structure and defers precise interpretation to a constrained elaboration step followed by tactic scripts.

Figure from the paper full image
abstract click to expand
Auto-formalization aims to translate informal mathematical content into formal languages that can be processed by theorem provers. However, directly targeting existing theorem provers requires LLMs to bridge a substantial representational gap between informal mathematical writing and formal proof languages. This gap also makes semantic consistency difficult to evaluate. We address these difficulties by introducing a Relaxed Natural Formal Language (Relaxed NFL) as an intermediate target for auto-formalization. The Relaxed NFL is designed to remain close to informal mathematical writing: it preserves the usual structure of informal reasoning and allows partially specified expressions and propositions, without requiring their precise interpretation to be fixed at the auto-formalization stage. The remaining ambiguity and implicitness inherited from informal reasoning are resolved during a later elaboration stage, which transforms Relaxed NFL proofs into Core Natural Formal Language (Core NFL) proofs with formally defined semantics. The elaboration procedure combines rule-based transformations with LLM-generated heuristics, while maintaining verifiability through explicit constraints on each transformation step. The Core NFL is then used to generate proof gaps, namely verification conditions that must hold for the formalized proof to be correct. These gaps are discharged by LLM-generated proof scripts written in a domain-specific tactic language, which provides commands for invoking theorem libraries and domain-specific solvers implemented as part of our system.
0
0
cs.PL 2026-06-23

Tool verifies safety in unbounded actor protocols if rounds stay bounded

by Christian Fontenot, Gowtham Kaki +1 more

DissProve: Automated Verification of Distributed Protocols with Affine Communication

Affine protocols admit goal-directed backward proofs that avoid global invariants and handle any number of participants.

Figure from the paper full image
abstract click to expand
We consider the problem of automatically proving safety properties of distributed protocols. Distributed protocols have been particularly challenging for automated verification due to their asynchronous and parametric nature. Compared to synchronous systems, asynchronous communication leads to a combinatorial explosion of possible execution histories of message handlers. And because distributed protocols are typically defined parametrically on the number of actors, these definitions lead to an unbounded number of possible execution histories of unbounded length. Existing verification techniques for such distributed protocols typically require global invariants about the entire actor system, which are complex even for simple protocols. In this paper, we present an automated verification technique based on proving unreachability backwards from error states in an actor system. One key insight is that the unboundedness from parametricity can be further classified into \emph{affine} and non-affine protocols, where affine protocols have execution histories of unbounded length in a bounded number of communication rounds. We show how to use novel, goal-directed notions of materialization, causality, and summarization to verify safety properties of affine protocols with an unbounded number of actors in an automated manner. Using our prototype verification tool DissProve, we provide evidence for the feasibility of automated safety verification of asynchronous parametrized systems with affine communication.
0
0
cs.PL 2026-06-23

One backend now verifies all three PLC program formats with unbounded proofs

by Pierre Dantas, Lucas Cordeiro +1 more

ESBMC-PLC+: A Unified IEC 61131-3 Formal Verification Framework as a PLCverif Successor

ESBMC-PLC+ adds Ladder Diagram support and k-induction to match PLCverif coverage while proving safety for any cycle count.

Figure from the paper full image
abstract click to expand
PLCverif is the most mature open-source platform for PLC formal verification, developed at CERN and in production use since 2019. Yet it has two fundamental limitations: no support for Ladder Diagram (LD) programs, the dominant PLC notation, and reliance on CBMC as its primary backend, which restricts verification to bounded proofs. The PLCverif authors themselves identified ESBMC as the appropriate backend improvement. Prior work established ESBMC-PLC (a textual LD frontend with k-induction) and ESBMC-GraphPLC (graphical PLCopen XML support); together, they cover LD with unbounded proofs but not Structured Text (ST), and graphical LD with timer/counter function blocks remains unverifiable. This paper presents ESBMC-PLC+, a unified framework that closes both gaps: (1) an ST/SCL frontend via the MATIEC IEC 61131-3 compiler, routing C-compiled ST to ESBMC with nondeterministic input modeling and YAML property injection; (2) function block state semantics for graphical LD, extending the DFS resolver to model TON/TOF/TP timers, CTU/CTD counters, and R_TRIG/F_TRIG edge triggers as persistent scan-cycle state variables in the GOTO IR. ESBMC-PLC+ is the first open-source PLC verification framework to support all three major IEC 61131-3 input formats via a single ESBMC backend, enabling k-induction-unbounded safety proofs. A feature comparison with PLCverif and experimental evaluation on 8 benchmark programs, including programs with up to 8 integer timers, shows that ESBMC-PLC+ matches PLCverif's input coverage while providing stronger guarantees. Against nuXmv's BDD backend, ESBMC-PLC+ is 400-2,000x faster on timer programs and completes proofs where nuXmv BDD times out at 120s.
0
0
cs.DB 2026-06-23

Compositionality added to graph queries for full NLOGSPACE expressivity

by Marcelo Arenas, Leonid Libkin +1 more

A Compositional Language for Property Graphs

Cleaned path queries with variables and #Datalog allow full mixing of graph and relational queries while building new graphs.

Figure from the paper full image
abstract click to expand
A major shortcoming of the recently standardized graph query languages GQL and SQL/PGQ is their lack of compositionality. Given the importance of these languages in querying knowledge graphs, we address this shortcoming and propose both theoretical solutions and a path to adding them to the new standards. The highlight of the non-compositionality problem is that while both GQL and SQL/PGQ can express graph reachability and all first-order queries, they fall short of the problems in NLOGSPACE. In view of the completeness of reachability for NLOGSPACE under first-order reductions, this is extremely counterintuitive. The issue is well recognized by the standards committee that has been searching for language extensions to fill the gaps at the level of some specific inexpressible queries. We address the issue in a systematic way and propose a language that fills expressivity gaps by allowing full compositionality between graph patterns and relational queries. It does so by using two key components: a cleaned up definition of regular path queries with variables and data value comparisons, and a fully compositional graph-to-graph language #Datalog with complete support for constructing new graph elements from nodes, edges, lists of nodes and edges, and even entire paths. We show that the resulting language addresses the issues facing the standards committee, and propose a concrete addition to GQL and SQL/PGQ that incorporates its main features.
0
0
cs.PL 2026-06-23

Tabling lets pure lambda calculus emit cyclic graphs

by Bo Yang

Cyclic Graphs and Memoization in Pure λ-Calculus

Weak-head tabling produces finite sound graphs for any finite-state term and performs automatic memoization.

Figure from the paper full image
abstract click to expand
Representing and transforming cyclic and infinite data in the pure $\lambda$-calculus normally requires an added recursion construct, a \texttt{letrec}, a $\mu$-binder, or a built-in $Y$ for graph reduction, and sharing the repeated work of a memoized or dynamic-programming function normally requires an impure cache. We show that no extension is needed. We apply tabling, the standard method for solving a least-fixpoint equation, to weak-head reduction; this defines a new operational semantics for the pure $\lambda$-calculus that keeps each term's standard lazy meaning. A term that reaches finitely many distinct states comes out as a finite graph, possibly cyclic; the calculus stays pure, and the graph is sound and independent of reduction order. We implemented this operational semantics as a $\lambda$-calculus interpreter. It does dynamic programming automatically, sharing repeated subproblems with no memoization table. It creates and transforms cyclic graphs with no added recursion construct. And it decides an unproductive loop, returning $\bot$ for $\Omega$ in finite time. What the evaluator returns is a graph, so the $\lambda$-calculus becomes a DSL for graph computation: the memo table of dynamic programming, the transposition table of game search, and the visited set of graph reachability and points-to analysis are all tabling on state identity, and none of them is written by hand. Compilation is one more such problem: we write a bootstrap compiler that compiles its own source, all as a pure $\lambda$-term.
0
0
cs.PL 2026-06-23

Lifting lets e-graphs treat functions as distinct from constants

by Philip Zucker

Lifting E-Graphs: A Function Isn't a Constant

Thinning bitvectors and a modified union-find keep alpha-canonical variables rigid inside the structure.

Figure from the paper full image
abstract click to expand
Variables are quite subtle and easy to get wrong. An approach is described to support rigid $\alpha$ canonical variables in an e-graph. The lifting e-graph has a baked-in notion of functional lifting combinator. It is implemented by fattening the usual integer identifiers with thinning bitvectors, lift-pulling smart constructors, and a special thinning-aware union find variation. The approach is inspired by slotted e-graphs and Co-de Bruijn syntax.
0
0
cs.PL 2026-06-22

Hedgehog forces sampling semantics for any compositional view

by Anthony Vandikas, Kiarash Sotoudeh +1 more

Compositional Generator Equivalence (Extended Version)

Arrow-calculus restriction regains a usable compositional distribution semantics while capturing practical generators.

Figure from the paper full image
abstract click to expand
Property-based testing (PBT) is a powerful technique for software verification that relies on random input generators and "shrinking" processes to find and minimize counterexamples to executable specifications called properties. While optimizing these generators is crucial for testing efficiency, formally justifying such optimizations is currently difficult because existing languages lack a compositional semantics that is coarse-grained enough for high-level reasoning. In this paper, we first provide a formal account of the syntax and semantics of Hedgehog, a popular PBT framework. We demonstrate that Hedgehog's distribution semantics - which models how users typically reason about generators - is non-compositional. Furthermore, we prove that any sound and complete compositional semantics for Hedgehog must necessarily be equivalent to its sampling semantics, which is too fine-grained to justify common program optimizations. To resolve this dilemma, we introduce Hedgehog$^\rightarrow$, a restricted version of the language based on the arrow calculus, and prove that Hedgehog$^\rightarrow$ possesses a compositional distribution semantics. We evaluate Hedgehog$^\rightarrow$ through a Haskell implementation and show that it remains expressive enough to capture generators of practical interest, while providing the formal foundation needed for compositional generator equivalence proofs.
0
0
cs.PL 2026-06-22

Synthetic domain theory yields powerdomains for nondeterminism

by Yue Niu, Taro Sekiyama

Powerdomains and nondeterminism in synthetic domain theory

The constructions give computationally adequate models that embed into dependent type theory for reasoning about programs.

Figure from the paper full image
abstract click to expand
Synthetic domain theory is an axiomatization of domain theory within a constructive universe of sets such that all definable maps between domains are continuous. In this paper we construct the counterparts to the well-known lower, upper, and convex powerdomains in the setting of synthetic domain theory and prove that they produce computationally adequate denotational models of nondeterminism. By developing the theory of powerdomains in synthetic domain theory, we obtain a nondeterministic metalanguage that directly embeds into dependent type theory, where the latter serves as an expressive logic for reasoning about the metalanguage. Moreover, the computational adequacy results imply that denotational reasoning through the metalanguage may be used to study operational behaviors of actual programs.
0
0
cs.PL 2026-06-22

Model counting quantifies precision loss across abstract domains

by Junda Zheng, Peisen Yao

Analyzing the Analyzers: Model Counting Meets Abstract Interpretation

Encodes concrete and abstract semantics as formulas to compute semantic loss directly, revealing intervals rival octagons and bit-level doma

Figure from the paper full image
abstract click to expand
Abstract interpretation offers a principled foundation for static analysis by approximating concrete program semantics via abstract domains. However, quantitatively comparing the precision of different domains remains a longstanding challenge. We present MCAI (Model Counting meets Abstract Interpretation), a new methodology that employs model counting to measure the precision of abstract domains. Unlike prior approaches that assess precision relative to specific analysis queries, MCAI encodes both concrete semantics and abstract values as logical formulas, enabling a client-independent, quantitative metric of imprecision that captures the inherent semantic loss in the abstractions. We apply MCAI to four abstract domains and evaluate the precision of their best abstract transformers via symbolic abstraction. Our results yield several insights: the Interval domain, despite its simplicity, often achieves precision comparable to that of Octagon; many octagonal constraints are semantically redundant; and the bit-level KnownBit domains consistently outperform the word-level domains. MCAI offers both theoretical insights into the precision of abstract domains and practical guidance for selecting suitable abstractions.
0
0
cs.PL 2026-06-22

No one strategy wins shared-context SMT batches

by Jiening Siow, Hanrui Zuo +3 more

Shared-Context Batched Satisfiability

Over-approximation wins easy symbolic abstraction cases while CLF handles more hard property checks.

Figure from the paper full image
abstract click to expand
Program analyzers often issue batches of SMT queries that share a large symbolic context and differ only in a small predicate. We formalize this recurring pattern as \emph{Shared-Context Batched Satisfiability}: given a formula $\varphi$ and predicates $P$, determine whether $\varphi \land p$ is satisfiable for each $p \in P$. We study three theory-agnostic strategies for this problem: predicate-by-predicate checking, disjunctive over-approximation, and Core-Literal Filter (CLF), a new algorithm that learns literals inconsistent with $\varphi$ and uses them to reject later predicates. Our evaluation on symbolic abstraction and active property checking shows that no strategy dominates universally: over-approximation is fastest on solved symbolic-abstraction queries, while CLF increases the number of solved hard instances and is fastest on active property checking. We advocate treating shared-context batched satisfiability as a first-class primitive in design program analyzers and exploring the algorithmic design space more systematically.
0
0
cs.PL 2026-06-22

LLMs generate CN memory specs for C programs at 97% success

by Twain Byrnes, Mike Dodds

CNnotator: LLM-Guided Memory Safety Annotation Synthesis

CNnotator automates annotation of implicit memory usage, reaching high success rates on small-to-medium code and suggesting broader practica

Figure from the paper full image
abstract click to expand
Memory safety errors account for a large proportion of security bugs in systems written in C; modern languages such as Java and Rust prevent such bugs because they are memory-safe by design. To migrate systems to safer languages or identify memory errors, we must first determine how legacy code manipulates memory. This information is only represented implicitly in such code. In many cases, memory usage patterns are merely tedious for humans to figure out, rather than truly difficult. In this work, we ask if large language models (LLMs) can perform this task by having them synthesize annotations representing memory usage as specifications in CN, a hybrid testing/verification tool. Our tool, CNnotator, uses LLMs to automatically generate and test CN specifications. We find that current models are able to generate CN specifications for small-to-medium C programs, with the OpenAI o3 reasoning model achieving a 90% success rate on first attempts and 97% overall success, while the chat model GPT-4o correctly annotates 65% of first attempts. These results suggest AI-assisted annotation is becoming practical for real-world C codebases.
0
0
cs.PL 2026-06-22

Symbolic SOS rules yield correct and complete symbolic execution

by Erik Voogd, Einar Broch Johnsen +3 more

Correct and Complete Symbolic Execution for Free

One rule format produces matching concrete and symbolic semantics without separate development.

Figure from the paper full image
abstract click to expand
Symbolic execution is a powerful technique for program analysis. However, the formal semantics underlying symbolic execution is often developed on an ad-hoc basis and decoupled from the concrete semantics of the programming language. To overcome this issue, we introduce symbolic SOS: a rule format that allows us to simultaneously specify concrete and symbolic operational semantics. We prove that symbolic semantics, when generated from symbolic SOS, is both correct and complete with respect to the corresponding concrete semantics. The approach relies only on an algebraic signature of the source language, and is thus language-independent.
0
0
cs.SE 2026-06-22

Incomplete constraints make constrained code gen worse than none

by Matteo Biagiola, Jahrim Gabriele Cesario +3 more

The Alignment Problem in Constrained Code Generation

Unconstrained decoding reaches higher functional correctness by avoiding low-probability regions created when constrainers reject valid prog

Figure from the paper full image
abstract click to expand
Large Language Models (LLMs) have demonstrated strong capabilities in code generation, but their outputs frequently contain syntax or type errors that result in compilation failures. Constrained decoding has been proposed as a solution to mitigate compilation errors by construction, improving functional correctness as a byproduct. However, previous works overlook a critical aspect of constrained decoding: the alignment between constrainer (e.g., types), language model and the target specification language (e.g., TypeScript). Misalignment is caused by the constrainer being incomplete--rejecting programs that belong to the target--or unsound--allowing programs that are not part of the target. The bias created by incompleteness distorts the language model distribution, and can be detrimental for code generation. We evaluate this hypothesis using seven language models, two target languages, two constrainers, enforcing types and syntax during decoding, and we study how language models react to varying levels of incompleteness. On three benchmarks, when the constrainer is incomplete, unconstrained decoding significantly outperforms constrained decoding in terms of functional correctness. Incompleteness pushes the model into low-probability regions of the program space, causing the generation to frequently time out, and reducing functional correctness by up to 97%. These contributions make the community aware of the negative effects of misalignment in constrained decoding, and provide quantitative insights on how to design constrainers that are beneficial for code generation systems with formal guarantees.
0
0
cs.SE 2026-06-22

KBSpec lifts LLM formal spec verification rates 10-25%

by Wenhan Wang, Zeyu Sun

KBSpec: LLM-driven Formal Specification Generation with Evolving Domain Knowledge Base

A knowledge base updated from verifier feedback on successful JML generations improves completeness without model tuning.

Figure from the paper full image
abstract click to expand
Automated formal specification generation is a key step towards program understanding and formal verification. Recently, due to the success of large language models (LLMs) in code generation, researchers have made early attempts to adopt LLMs for generating formal specifications. However, the lack of formal specification language corpora in the wild often makes LLMs fail to generate syntactically correct and semantically verifiable specifications. To mitigate this gap, we propose KBSpec, which augments LLMs with dual-source knowledge of formal specification language: external knowledge from official documentation, and internal knowledge distilled from verifier feedback on LLM-generated specifications. KBSpec maintains a self-evolving knowledge base that is continuously updated from successful generation and repair trajectories, without any LLM parameter tuning or labeled training data. We evaluate KBSpec on Java Modeling Language (JML) specification generation with three LLM backends, and results show that KBSpec improves verification pass rates by 10-25% over state-of-the-art LLM-based approaches, while producing the largest number of high-completeness specifications.
0
0
eess.AS 2026-06-22

Compiler turns trained audio models into matching FAUST plugins

by Facundo Franchino, Sebastian J. Schlecht

Compiling Differentiable Audio Graphs to Real-Time DSP

The generated real-time code replicates the model's impulse response within floating-point noise and includes built-in stability checks.

Figure from the paper full image
abstract click to expand
Differentiable audio processors are habitually designed and optimised in machine-learning frameworks, but deploying them as real-time audio effects still often requires non-automatic implementation in a dedicated digital signal processing language. The translation is error-prone, demands an onerous verification process, and detaches research prototypes from usable production tools. That being so, we present ADAC, a compiler that lowers a trained model to a framework-agnostic intermediate representation and emits efficient FAUST code whose impulse response matches the source model to within floating-point arithmetic noise, direct paths included. The optimisation loop is made audible by replacing the model in a running plugin after each gradient step. The exported processor carries a small set of macro-controls that leave its stability intact. A stability certificate computed from the shipped parameters is checked before the plugin is built. At the demonstration, a feedback delay network is trained and exported to a working plugin.
1 0
0
cs.PL 2026-06-22

AI reorganizes CertiGC proof around new invariant for mutable collector

by Shengyi Wang

AI-Assisted Completion of CertiGC Proofs: An Experience Report

Recorded-backward-edge requirement replaces invalidated no-backward-edge assumption and restores the top-level correctness theorem.

Figure from the paper full image
abstract click to expand
This experience report describes the Codex-assisted completion and stabilization of a substantial Rocq (formerly Coq) proof development for CertiGC, the verified generational garbage collector in the CertiGraph project. The development extends the collector from an effectively immutable setting to a mutable one by adding remembered-set forwarding to the collection path and re-establishing the top-level graph-isomorphism correctness theorem. The central technical issue was not low-level proof scripting alone: mutable updates invalidate the old global no-backward-edge assumption, so the proof had to be reorganized around a recorded-backward-edge invariant stating that every backward edge is recorded in the appropriate remembered-set component. This case differs from recent AI-assisted formal-proof accounts: unlike the adaptation of a nearby compilerproof architecture or a fresh metatheory formalization, it completes a long-running verification in a mature codebase built on the Verified Software Toolchain (VST) and CertiGraph, both mechanized in Rocq. The Rocq kernel remained the arbiter of correctness, while our role shifted toward adjudicating invariant proposals, constraining specification changes, reviewing theorem statements, and deciding when proof cleanup was justified. The Codex-assisted phase repaired the VST relation proofs first, then restored the mathematical graph-isomorphism theorem, and only then audited the premise path from the VST specification to the theorem. That audit found and removed a stale no-backward-edge condition from the VST-facing proof path. This report presents the workflow, resulting proof artifact, and lessons for agentic proof maintenance.
0
0
cs.PL 2026-06-19

Horn clause programs convert between big-step and small-step forms

by John P. Gallagher, Manuel Hermenegildo +3 more

Big-step and small-step Horn clause derivations applied to operational semantics

Interpreter specialization yields equivalent clause sets, turning big-step language semantics into small-step versions.

abstract click to expand
The concepts of big-step and small-step derivations are familiar from the operational semantics of programming languages. These concepts are applicable in the more general setting of Horn clause derivations. We prove equivalence between big-step derivations and two versions of small-step derivations for Horn clauses. By specialising interpreters for these derivation strategies, any set of Horn clauses can be transformed into a provably equivalent set of clauses that inherits the behaviour of a given (big- or small-step) Horn clause interpreter. As a special case of this transformation, big-step semantics for any programming language, expressed directly as Horn clauses, can be transformed into equivalent small-step semantics. Experiments with a variety of programming languages are reported.
0
0
cs.AI 2026-06-19

Multi-LCB shows LLMs overfit to Python on code tasks

by Maria Ivanova, Pavel Zadorozhny +6 more

Multi-LCB: Extending LiveCodeBench to Multiple Programming Languages

Extending LiveCodeBench to twelve languages uncovers performance gaps while retaining contamination controls.

Figure from the paper full image
abstract click to expand
LiveCodeBench (LCB) has recently become a widely adopted benchmark for evaluating large language models (LLMs) on code-generation tasks. By curating competitive programming problems, constantly adding fresh problems to the set, and filtering them by release dates, LCB provides contamination-aware evaluation and offers a holistic view of coding capability. However, LCB remains restricted to Python, leaving open the question of whether LLMs can generalize across the diverse programming languages required in real-world software engineering. We introduce Multi-LCB, a benchmark for evaluating LLMs across twelve programming languages, including Python. Multi-LCB transforms Python tasks from the LCB dataset into equivalent tasks in other languages while preserving LCB's contamination controls and evaluation protocol. Because it is fully compatible with the original LCB format, Multi-LCB will automatically track future LCB updates, enabling systematic assessment of cross-language code generation competence and requiring models to sustain performance well beyond Python. We evaluated 24 LLMs for instruction and reasoning on Multi-LCB, uncovering evidence of Python overfitting, language-specific contamination, and substantial disparities in multilingual performance. Our results establish Multi-LCB as a rigorous new benchmark for multi-programming-language code evaluation, directly addressing LCB's primary limitation and exposing critical gaps in current LLM capabilities.
0
0
cs.LO 2026-06-19

Cubical Agda verifies d-separation on every finite DAG

by Karen Sargsyan

A cubical formalisation of conditional independence, Bayesian conditioning, and Pearl's d-separation soundness

Generalized interchange axiom for finite distributions enables proofs of semi-graphoid axioms, do-calculus and Markov category properties wi

abstract click to expand
The standard convex-algebra interchange axiom, common to probability-monad formalisations since Stone, is provably too weak to support full Bayesian conditioning. We make this precise in Cubical Agda: finite distributions as a higher inductive type, conditional independence as a cubical path between kernels, recursive Bayesian conditioning as a total function on a full-support fragment. Lifting conditioning to the full HIT exposes a structural mismatch -- the two halves of the rearranged 4-leaf mix carry distinct Bayesian weights related by Bayes' formula, not the single shared inner weight the standard axiom provides. We exhibit the minimal generalisation that resolves this and prove the standard form is the degenerate case where the two inner weights coincide. Around this observation we verify the algebraic context constructively, with zero postulates above an abstract ordered-field interface: bind commutativity, the four semi-graphoid axioms, intersection (reduced to contraction via structural $\Sigma$-witnesses, without positivity), Pearl's do-calculus Rules~1, 2, and~3 in kernel form, finite-type Bayesian conditioning, and Pearl's d-separation theorem (soundness) on arbitrary $n$-vertex finite directed acyclic graphs (DAGs) in both interventional and Bayesian forms. The probability monad is also verified as a Markov category; the abstract interface discharges at $Q$.
0
0
cs.LO 2026-06-19

SC executions have bounded treewidth

by Giovanna Kobus Conrado, Andreas Pavlogiannis

An MSO Framework for Weak-Memory Verification and Robustness

This split lets MSO express some memory models for uniform verification and robustness checks but rules out others unless a quadratic-time p

abstract click to expand
Memory models are formal specifications of concurrent-program executions, accounting for weak behaviors introduced by compiler and architectural optimizations. The increase of their number and complexity has spawned efforts for uniform verification across whole classes of models, by axiomatizing the models in an adequate metatheory that admits a uniform treatment. In this work, we formally study Monadic Second-Order logic (MSO) as a metatheory for weak memory, by proving results on the treewidth and MSO-expressibility of various popular weak-memory models, as this combination allows us to uniformly tackle several verification problems. In summary, our results are as follows. First, we prove that executions under Sequential Consistency ($\mathsf{SC}$) have bounded treewidth, while already those under Total Store Order ($\mathsf{TSO}$) do not. Second, we prove that a broad range of models, including Release/Acquire and the full RC20, are MSO-axiomatizable, while others, such as Strong Release/Acquire and $\mathsf{TSO}$, are not, unless the Orthogonal Vectors problem $\unicode{x2013}$ which requires quadratic time under SETH $\unicode{x2013}$ can be solved in linear time. Finally, we introduce the notion of reads-from robustness, as an extension to recent work on coarse robustness criteria. We show that our treewidth bounds (both upper and lower) have far-reaching algorithmic implications for any of our MSO-axiomatizable models $\mathsf{MM}$: there is an algorithm that, for every program $\mathsf{P}$, either verifies $\mathsf{P}$ under $\mathsf{MM}$ or reports that $\mathsf{P}$ is not reads-from robust against $\mathsf{MM}$. Overall, our results establish a rich and versatile theoretical framework for weak-memory verification and robustness.
0
0
cs.PL 2026-06-19

Effect systems recovered as abstract interpretations on events

by Colin S. Gordon

Effect Systems as Abstract Interpretations

Embedding effect quantales shows they arise from interpreting event sequences rather than program states.

Figure from the paper full image
abstract click to expand
Many forms of static reasoning about program behaviours are known in the literature, yet formal relationships are studied surprisingly infrequently. While most type systems are well-known to be captured by abstract interpretations, the situation for type-and-effect systems is, in the general case, unsettled despite strong hypotheses and occasional framing of effect systems as abstract interpretations. We develop a formal relationship between abstract interpretations and a general class of effect systems. First, we describe an embedding of effect quantales into abstract domains. Second, we recover the general form of an effect quantale as an abstract interpretation -- not on states or values, but on event occurrences.
0
0
cs.PL 2026-06-18

Semantic framework stabilizes quantum outputs across backends

by Jaime Alexander Jimenez Lozano, Sebastian Jimenez Giraldo

QDSV: A Semantic Problem Representation and Multi-Backend Execution Framework for Quantum-Oriented Computation

EEG case study shows consistent interpretable traces from simulator to IBM hardware without circuit authoring.

Figure from the paper full image
abstract click to expand
Predicate-based computation over state spaces separates a problem specification from the backend that realizes it. Building on the model introduced in arXiv:2606.15027, this paper studies QDSV as a semantic, multi-backend execution framework for quantum-oriented computation. We describe how QDSV, QIntent, and Qruba connect declarative problem intent to a structured semantic representation, realize that representation under heterogeneous backend constraints, and report execution trace outputs that separate model-level semantic outputs from backend-specific observations. The framework supports execution modes that do not require the original problem to be authored as a circuit, while still allowing circuit-compatible artifacts when required. As a case study, we evaluate EEG ictal/interictal classification using prepared signal features from the Bonn and Delhi datasets. The study compares classical machine-learning references, a circuit-first variational quantum classifier baseline, QDSV simulator executions, and controlled IBM Quantum hardware runs. The paper does not claim general quantum advantage or superiority over classical machine learning. Its contribution is a semantic execution validation showing how a problem-first representation can remain stable across simulator and hardware realizations while retaining interpretable execution trace outputs.
0
0
cs.SE 2026-06-18

Session carries agent state as first-class runtime value

by Fukang Wen, Zhijie Wang +1 more

OpenRath: Session-Centered Runtime State for Agent Systems

Making fork, merge, and replay explicit operations instead of external trace reconstructions.

Figure from the paper full image
abstract click to expand
Modern agent systems often suffer from fragmented runtime state: transcripts, tool effects, memory events, workspace placement, branch provenance, and replay evidence are recorded separately and become difficult to inspect or reproduce. OpenRath addresses this issue with a PyTorch-like programming model for multi-agent, multi-session systems. The analogy concerns the role of a central first-class runtime abstraction, not tensor computation. Its core abstraction is Session, the runtime value passed between agents and workflows. A Session is branchable, inspectable, replayable, backend-aware, and composable. It records conversation chunks, sandbox placement, lineage metadata, token usage, pending work, and tool evidence, while defining where memory interactions enter the runtime record. Since this state is carried by the same value used in program execution, fork, merge, and replay become explicit runtime operations rather than states reconstructed from external traces. OpenRath further defines Sandbox, Tool, Agent, Memory, Workflow, and Selector, with Selector turning control flow into runtime-routed decisions. This report presents the programming model, architecture, audited milestones, and evidence protocol. Its claims are limited to controlled runtime properties, while broad quantitative comparisons, live-provider quality, optional-backend availability, and memory quality are left for follow-on evaluation. The central thesis is that Session provides agent systems with a first-class runtime value for auditable composition.
0
0
cs.PL 2026-06-18

DFS resolver converts graphical PLC ladders to verifiable IR

by Pierre Dantas, Lucas Cordeiro +1 more

ESBMC-GraphPLC: Formal Verification of Graphical PLCopen XML Ladder Diagram Programs Using SMT-Based Model Checking

Graphical exports from CONTROLLINO and OpenPLC Editor now produce full GOTO programs that the SMT checker can examine instead of empty IR.

Figure from the paper full image
abstract click to expand
PLCopen XML defines two encoding formats for IEC 61131-3 Ladder Diagram programs: a textual encoding using <rung> elements, and a graphical encoding that represents rung logic as a directed graph of localId/refLocalId connections. ESBMC-PLC supported the textual format but parsed graphical exports from CONTROLLINO, Beremiz, and OpenPLC Editor into an empty GOTO intermediate representation, causing vacuous verification success. This paper presents ESBMC-GraphPLC, which closes this gap with a DFS-based graphical LD resolver. The resolver traverses the connection graph from leftPowerRail to each coil, extracts rung paths as Boolean contact conjunctions, and applies a three-tier I/O inference scheme. Ordering coils by rightPowerRail connectionPointIn sequence ensures SET coils process before RESET coils, matching IEC scan-cycle semantics. The graphical-to-IR conversion leaves the ESBMC backend unchanged. Validation on 3 graphical LD programs from CONTROLLINO/OpenPLC Editor shows all produce full GOTO IR with nondeterministic inputs and rung logic, versus the empty IR previously. All 3 verify SAFE at k=2 under 70ms. The 11 textual LD benchmarks are fully preserved, with no regression. Two Beremiz examples with no LD content or unsupported timer semantics are reported as discovered limitations. Artifact at Zenodo (DantasCordeiro2026graphical, doi:10.5281/zenodo.20699856).
0
0
cs.LG 2026-06-18

Verifier feedback lifts theorem proving to 40.6% on miniF2F

by Manish Acharya, Zhenyu Liao +4 more

VERITAS: Verifier-Guided Proof Search for Zero-Shot Formal Theorem Proving

Two-phase protocol turns Phase-1 failures into MCTS negatives and adds solves on both miniF2F and a new combinatorics set without losing ear

Figure from the paper full image
abstract click to expand
LLM-based formal provers often collapse rich verifier signals (syntax errors, type mismatches, partial goal progress) into a binary pass/fail bit. We present VERITAS, a zero-shot framework that routes every verifier signal back into proof search through a two-phase protocol: Best-of-N sampling first, then a critic-guided MCTS pass that ingests Phase 1 failures as explicit negative examples. The protocol preserves every theorem solved by its own Phase 1 sweep, so Phase 2's additional solves are attributable to feedback-driven exploration. VERITAS reaches 40.6% on miniF2F (vs. an independently run Best-of-5 at 36.9%, Portfolio 26.2%) and 7.3% on VERITAS-CombiBench, a 55-theorem combinatorics benchmark we release on which Best-of-5 (1.8%) falls below Portfolio (3.6%), exposing that unguided sampling hurts when correct lemma names must be recovered iteratively from verifier feedback. Artifacts are available on GitHub.
0
0
cs.PL 2026-06-17

C and C++ fastest for AI algorithms

by Juan P. Licona-Luque, Beatriz A. Bosques-Palomo +5 more

Behind Python: The Languages That Power AI

Five algorithms benchmarked in six languages show Rust close behind and rankings that shift by workload.

Figure from the paper full image
abstract click to expand
Python dominates AI development, yet the numerical work behind frameworks like PyTorch and NumPy is executed in C, C++, or Rust. When a developer must implement an algorithm without such libraries -- because none exists, the target is resource-constrained, or a new system is being built -- which language should they choose? This paper answers that question empirically. Five algorithms covering data mining (k-means), machine learning (k-NN), neural networks (MLP with backpropagation), computational intelligence (genetic algorithm), and fuzzy systems (Mamdani inference) are implemented from scratch in Python, C, C++, Rust, Go, and Julia. All implementations share a common pseudo-random generator, consume identical inputs, and produce bit-identical outputs, so every measured difference reflects the language rather than the computation. Three performance tiers emerge: C and C++ are effectively tied; Rust trails them by 9% (geometric mean); Julia runs 3.3x slower than C and Go 5.0x; Python sits at 315x. Memory tells a different story -- Julia's JIT runtime carries a fixed ~224 MiB footprint regardless of workload, while C, C++, and Rust stay below 6 MiB. Crucially, rankings are not stable: Go's slowdown swings from 2.6x on k-NN to 8.0x on k-means, showing that workload characteristics can shift a language's position by a full tier. The results provide concrete, per-workload guidance for choosing an implementation language in AI systems.
0
0
cs.PL 2026-06-17

Runtime checks guard Move contracts against verifier errors

by Victor Gao, Wolfgang Grieskamp +6 more

Defense-in-Depth Runtime Safety in Move

Aptos blockchain performs independent execution-time verification of invariants to block asset loss from static analysis flaws.

Figure from the paper full image
abstract click to expand
Move is a smart-contract language used to execute transactions on the Aptos blockchain. Move programs execute in a sandboxed VM as typed bytecode. The VM statically verifies foundational safety properties like type safety and reference safety at code loading time. In principle, this design gives strong guarantees for Move. However, the static verification logic is complex and continually evolving with the language; like any software, it is not immune to bugs. In a live blockchain setting, a missed rule violation can translate directly into loss of assets, forged authority, or unrecoverable corruption of on-chain state. For this reason, Aptos relies on defense-in-depth runtime safety checks that independently verify the critical invariants during execution, providing protection against latent verifier bugs and malicious bytecode. This paper motivates and describes the runtime safety checks for Move on Aptos.
0
0
cs.CL 2026-06-17

SwiftTrans boosts correctness and speed in LLM code translation

by Longhui Zhang, Jiahao Wang +4 more

Bridging Functional Correctness and Runtime Efficiency Gaps in LLM-Based Code Translation

Two stages generate diverse candidates then select the optimal by comparing differences, with gains on three benchmarks.

Figure from the paper full image
abstract click to expand
While large language models (LLMs) have greatly advanced the functional correctness of automated code translation systems, the runtime efficiency of translated programs has received comparatively little attention. With the waning of Moore's law, runtime efficiency has become increasingly important for program quality, alongside functional correctness. Our preliminary study reveals that LLM-translated programs often run slower than human-written ones, and this issue cannot be remedied through prompt engineering alone. Therefore, our work proposes SwiftTrans, a code translation framework comprising two key stages: (1) Multi-Perspective Exploration, where MpTranslator leverages parallel in-context learning (ICL) to generate diverse translation candidates; and (2) Difference-Aware Selection, where DiffSelector identifies the optimal candidate by explicitly comparing differences between translations. We further introduce Hierarchical Guidance for MpTranslator and Ordinal Guidance for DiffSelector, enabling LLMs to better adapt to these two core components. To support the evaluation of runtime efficiency in translated programs, we extend existing benchmarks, CodeNet and F2SBench, and introduce a new benchmark, SwiftBench. Experimental results across all three benchmarks show that SwiftTrans achieves consistent improvements in both correctness and runtime efficiency.
0
0
cs.PL 2026-06-17

Visored turns LLM natural-language proofs into Lean-checked files

by Xiyu Zhai, Xinyi Chen +4 more

Visored: A Controlled-Natural-Language Prover for LLM-Generated Mathematics

A rule-driven automation layer fills omitted steps so accepted proofs export as verified Lean code, and LLMs use the system on miniF2F witho

Figure from the paper full image
abstract click to expand
We present a dependent-type-based prover designed around the way LLMs (and humans) tend to write mathematics, complementing existing systems such as Lean and Rocq. Its core design choices are a surface that imitates mathematical natural language and a rule-driven automation layer that closes the routine steps a textbook would omit, so that an accepted proof can be re-emitted as a checked Lean file. Early experiments suggest that, even without any prover-specific training data, LLMs can learn to use it effectively on the miniF2F benchmark. Lean output excerpts: https://github.com/xiyuzhai-husky-lang/visored/
0
0
cs.LG 2026-06-17

Distribution training on Go traces reaches 36.2% next-step accuracy

by Kaviru Hapuarachchi

When the Next Step Is Not One Step: Distribution-Aware Execution Modeling for Concurrent Go Programs

Fewer than 1000 traces let a 7B model beat zero-shot Gemini while cutting calibration error on real concurrency bugs

Figure from the paper full image
abstract click to expand
Training a model to predict the next step in a concurrent program is harder than it looks: two runs of the same program from the same trace prefix can produce different next events, both valid, because the scheduler is nondeterministic. A model trained against a single label is learning to guess one outcome of a random process. We turn this around and use the nondeterminism as a training signal. We run each program many times, aggregate the observed next events into an empirical distribution, and fine-tune a 7B model to match that distribution with a KL objective. On 798 held-out predictions drawn from real production Go bugs (CockroachDB, Kubernetes, gRPC, etcd), fine-tuning on fewer than a thousand traces reaches 36.2% accuracy, ahead of Gemini 3.5 Flash used zero-shot (34.8%) and the same model without fine-tuning (28.6%). Distribution training matches cross-entropy on accuracy (35.8% vs. 36.2%) while reducing Expected Calibration Error from 0.205 to 0.169. We also derive a formal goroutine-leak signature for a class of select-blocked goroutines where P(GoUnblock)=0 holds by scheduler semantics, not by learning. We release the dataset, trained adapters, and all tooling.
0
0
cs.LO 2026-06-17

Crowdsourced proofs verify large parts of Rust std library

by Byron Cook, Remi Delmas +10 more

Verifying the Rust Standard Library

An open campaign folds multiple tools into CI to produce machine-checked guarantees against out-of-bounds access and related undefined behav

Figure from the paper full image
abstract click to expand
Rust's type system prevents many classes of memory errors, yet its standard library relies heavily on unsafe code whose correctness is validated through testing, including dynamic checks under Miri, but lacks static verification. We present what is, to the best of our knowledge, the largest verification campaign reported for a software library: an open, crowdsourced effort that integrates complementary verification tools into the continuous integration of a verification repository forked from the Rust standard library. We analyze the campaign's effectiveness, discuss the practical value of machine-checked proofs for a subset of undefined behaviors (e.g., out-of-bounds access, null and dangling pointer dereferences, and use of uninitialized memory), and frame the remaining obstacles as open challenges for the formal-methods community.
0
0
cs.LO 2026-06-16

Stone-Cech compactification separates four divergence types in CCS

by Mike Stannett

A Stone-Cech Collecting Semantics for Residual Process Behaviour

Tail-cluster sets of residual streams distinguish stable, recurrent, mixed and escaping nontermination while validating prefix and choice la

abstract click to expand
This paper develops a compact collecting semantics for the residual behaviour left by nonterminating computation. For sequential time this is the tail-cluster set of the stream in the Stone-Cech compactification of the observation space. It gives a common semantics to ordinary recurrence, mixed recurrent behaviour, and escape through noncompact parts of the observation space. The basic theory establishes tail invariance, functoriality under continuous observations, and a temporal reading for clopen observations: containment in the corresponding clopen region of beta-X is eventual truth, while nonempty intersection is recurrence. Progress and fairness assumptions are represented by strengthening the time filter. Relational meanings are obtained by compactifying products, so correlations between observations made along the same asymptotic view of time are retained. The main application is to residual behaviour in CCS. Infinite executions are read as streams of residual processes modulo structural congruence. The resulting semantics distinguishes stable divergence, finite recurrent divergence, mixed recurrence with escape, and escape through unbounded residual growth. It validates residual-tail laws for prefixing, guarded unfolding, finite choice, and finite prefix-choice forms, while also identifying the boundary of those laws under parallel composition and synchronisation. Finite observational quotients provide the computational interface to the compact semantics: abstract meanings become recurrent states and strongly connected component calculations, and resource observations detect unbounded escape without requiring individual points of the Stone-Cech remainder to be inspected.
0
0
cs.LG 2026-06-16

Verus proofs establish detectors for four LLM agent anomalies

by Sajjad Khan

Verified Detection and Prevention of Concurrency Anomalies in Multi-Agent Large Language Model Systems

A verified chain L0 to L4 supplies sound prevention for stale-generation, phantom-tool, causal-cascade and tool-effect reordering.

Figure from the paper full image
abstract click to expand
Multi-agent LLM systems share state through memory stores, vector indices, and tool registries. We model such sharing as long-running read-generate-write operations under deterministic-generation semantics -- the regime durable-execution engines enforce by deterministic replay -- and formalize four concurrency anomalies in TLA+: stale-generation, phantom-tool, causal-cascade, and tool-effect reordering, structural analogues of classical isolation anomalies, each with a TLC counter-example. The exclusion lattice over these anomalies is trivial; the contribution is the mechanically verified realizability and strict separation of one maximal chain within it, $L_0 \subsetneq \cdots \subsetneq L_4$, to our knowledge the first machine-checked consistency hierarchy for such runtimes. A development of 274 Verus obligations (zero assume, zero admit; trust base: two structural axioms and a mutex correspondence) proves the detectors sound and complete against the specifications and each runtime its avoidance set. Three deployed Rust runtimes realize L0-L1 (pessimistic locking, serializable snapshot isolation, default-SI), each verified against stale-generation and refined to its state machine; L2-L4 are exec-mode-verified with dependency-free prevention twins (A3, A6, A2: 0/1000 versus 1000/1000), and L2 is run live across three model families (A3 prevented in all 120 retracted sessions). We reproduce a silent lost update in ByteDance's deer-flow, formalizing its fix as a verified $L_0 \to L_1$ refinement, and exhibit tool-effect reordering in LangGraph's ToolNode on unmodified output, removed by an L3 commit-order sequencer. The verified detector, refinements, and realizability artifacts are the contribution; the phenomena and lattice are classical.
0
0
cs.CL 2026-06-16

Percent-prefixed directives let models handle complex prompts without tuning

by Enkhzol Dovdon

PromptMN: Pseudo Prompting Language

PromptMN annotates natural language with typed instructions so models resolve roles, goals, conditionals, and prime checks reliably.

Figure from the paper full image
abstract click to expand
Prompting has become the primary interface between humans and generative AI, yet many natural language prompts remain fragile: roles, goals, constraints, and expected outputs are often buried in prose or left implicit. In agentic and software development workflows, a misread at the first handoff can propagate through every step, since a significant portion of agent failures stem from context ambiguities rather than model limitations. This paper introduces PromptMN, a pseudo-prompting domain-specific language that annotates natural language with compact, %-prefixed typed directives covering roles, goals, requirements, priorities, constraints, plans, inputs, and outputs. Semantic resolution lets authors write in any order while the model interprets directives by function. PromptMN sits between informal prompting and programming-style pseudocode: structured enough to be inspectable and reusable, yet lightweight enough for analysts, managers, developers, and stakeholders across the software development lifecycle (SDLC). PromptMN also pairs with reverse prompt engineering. Asking a model to restate a desired outcome as PromptMN lets users inspect the inferred roles, goals, constraints, and missing assumptions before acting, reducing repair cycles and yielding a reusable artifact for aligning people and AI tools. PromptMN's feasibility is evaluated across several frontier models, including Claude Fable 5, Claude Opus 4.8, Gemini 3.1 Pro, and GPT-5.5. The models correctly resolved PromptMN instructions, including complex structures such as repetition, conditionals, methods, and a prime-checking task, without fine-tuning. The same vocabulary applies across new codebases, maintenance, and redesign in the SDLC scenarios presented. While large-scale validation remains future work, these early results suggest PromptMN is a practical step toward clearer, more reviewable human-to-AI interaction.
0
0
cs.PL 2026-06-15

ScratchLens achieves zero false equivalences on Scratch mutation corpus

by Yuan Si, Jialu Zhang

ScratchLens: Lens-Parametric Behavioral Equivalence for Scratch Programs

Causal IR plus trace quotients classify all 444 validated pairs from real projects and record none on 158 witnessed-different ones.

Figure from the paper full image
abstract click to expand
Two Scratch programs can be syntactically far apart-renamed variables, split scripts, extracted custom blocks, or reordered initialization-and still behave identically; a one-block edit, such as replacing a blocking broadcast with an asynchronous one, can create divergences visible only under specific schedules. Deciding behavioral equivalence is central to automated feedback, grading support, and repair validation, yet tree differencing is too strict and single-run dynamic comparison is unsound for concurrent, random, and timing-dependent behavior. We observe that equivalence for block-based programs is lens-parametric: final state, frame traces, monitors, event causality, and debug traces induce different observation relations. ScratchLens makes this explicit through a taxonomy of causal divergence phenomena and observation lenses. It compiles Scratch projects into a causal IR of typed resources and semantic transactions, canonicalizes renamings, guards, and procedure bodies, quotients same-trigger concurrency with Mazurkiewicz trace normal forms, separates program order from races, and handles residual frontiers through SMT obligations and VM-backed counterexample-guided refinement. Conclusive verdicts carry evidence: equivalence by bijection and trace quotient, difference by a typed witness, and unresolved cases remain unknown. On a VM-witnessed mutation corpus from real Scratch projects, ScratchLens decides all 444 validated pairs and makes 0/158 false-equivalence claims on witnessed-different pairs under strict scoring. Structural, dynamic-only, and LLM baselines fail on the classes predicted by the taxonomy; ablations quantify the contribution of partial-order reduction and lens parametricity; and targeted scenarios expose ambiguous-mutant divergences missed by random testing.
5 0
0
cs.PL 2026-06-15

Decision diagrams scale probabilistic program checks by orders of magnitude

by Daniel Basgöze, Kevin Batz +2 more

Scalable Probabilistic Program Verification via Typed Extended Decision Diagrams

TEDDs keep weakest pre-expectations compact on loops, enabling SMT pruning where prior methods ran out of memory.

Figure from the paper full image
abstract click to expand
Weakest pre-expectations are the probabilistic program analogue to weakest preconditions in classical programs. Deductive verification approaches aim to establish bounds on these quantitative expectations. Their automation has been successful in analysing a variety of discrete probabilistic programs. Key routines in that automation require reasoning about (partially unrolled) loops, however, the logical representation of weakest pre-expectations on such unrollings often explodes. In this paper, we develop typed extended decision diagrams (TEDDs), inspired by various extensions to binary decision diagrams. We demonstrate computing WPs represented as TEDDs, SMT-based pruning to further shrink their representation, and we lift some proof rules to operate on TEDDs. Finally, we demonstrate that TEDDs boost the scalability of deductive probabilistic program verification by orders of magnitudes over the state of the art.
0
0
cs.PL 2026-06-15

Python package runs models directly on Apple Neural Engine

by Spencer H. Bryngelson

ANEForge: Python for direct computation on the Apple Neural Engine

Compiles lazy tensor graphs to native ANE programs that finish ResNet-18 forward passes in 0.33 ms and support training.

Figure from the paper full image
abstract click to expand
ANEForge is a Python package that programs the Apple Neural Engine (ANE), the fixed-function neural accelerator on every recent Apple device, directly and without CoreML. In production the engine is reachable only through CoreML, which treats it as a scheduling option: no configuration requires the ANE, and a model can silently run on the CPU or GPU instead. ANEForge compiles a lazy tensor graph, built from 58 fused operators and 19 native bridge operators, into a single ANE program. The program is dispatched through the same ANE daemon and kernel-driver stack as Apple's internal framework. Beyond inference, the package reaches the engine's native fused attention, streams int8, int4, and sparse weights, keeps decoder and optimizer state resident across steps, and runs the forward pass, backward pass, and optimizer update of training on the engine. A small fused program completes a call in about 90us, near the engine's 70us per-program dispatch floor, and a pretrained ResNet-18 forward runs end-to-end in 0.33ms. ResNet-18, a sentence encoder, and a Vision Transformer run end-to-end against framework references, and a Stable Diffusion U-Net validates its forward pass. ANEForge targets Apple Silicon under macOS 14 and later. Each release is verified against a recorded macOS and ANE-compiler version.
0
0
cs.PL 2026-06-12

One program drives and monitors hardware protocols

by Ernest Ng, Nikil Shyamsunder +3 more

Specifying Hardware Communication as Programs

A DSL encodes a protocol once as an imperative script; the same script generates signals and reconstructs transactions from waveforms.

Figure from the paper full image
abstract click to expand
To test and debug hardware modules, it is common to write two programs: a driver, which translates high-level transactions into interactions on the module's input and output signals, and a monitor, which analyzes a signal-level execution trace and recognizes a transaction. These two programs are commonly implemented separately for each hardware protocol, but this separation entails manual effort and risks inconsistencies. We advocate an alternative approach. We present a DSL in which users specify hardware communication protocols as succinct imperative programs. Crucially, the same specification can be used to both drive designs and monitor transactions. We present the design of a tool, which given a specification in our DSL and a waveform, automatically infers a transaction-level trace consistent with the waveform. We discuss plans to evaluate our DSL on real-world interconnects such as Wishbone and AXI-Stream.
0
0
cs.PL 2026-06-12

AsInst models choreographies as temporal Bayesian networks

by Mako Bates, Steven Baldasty +3 more

Probabilistic, Resource-Aware, Asynchronous, Out-of-Order Choreographies

Programs yield networks that track values and availability times under delays, failures, and recovery.

Figure from the paper full image
abstract click to expand
Futures-based implementations of out-of-order choreographies can substantially improve latency and throughput, but their actual behavior depends on resources such as communication delay, computation time, failures, and recovery. Existing formal models such as Ozone's O3 describe which executions are possible, but do not directly explain how likely those executions are or how long they take. In this work we present AsInst, a probabilistic, resource-aware language for modeling the semantics of asynchronous choreographies with out-of-order execution. AsInst programs are interpreted as temporal Bayesian networks that model both the values produced at runtime and the times at which they become available. We prove that this central semantics correctly captures a corresponding futures-style network semantics. We also show that AsInst can encode Ozone-style select-and-merge conditionals, and we use case studies to model communication-failure recovery and analyze runtime performance.
0
0
eess.AS 2026-06-12

Faust DSP compiles to CLAP with live edit support

by Facundo Franchino (1), Stéphane Letz (2) +3 more

A Dual-Mode Faust-to-CLAP Compilation System

Static and dynamic modes keep parameters stable during code changes without host restarts.

Figure from the paper full image
abstract click to expand
We describe faust2clap, a framework establishing the first officially maintained compilation pathway from Faust DSP specifications to the CLAP format. The system operates in two different modes. A static mode employs ahead-of-time compilation to yield native binaries of optimal efficiency, while a dynamic mode uses runtime interpretation to permit DSP code modification without interrupting the host application. This latter capability addresses a persistent friction in audio software development, namely the cumulative overhead of the edit, compile, and reload cycle. We detail the algorithmic machinery underlying both modes, focusing specifically on the problem of parameter identity. To preserve both parameter values and their bindings to host automation across structural DSP mutations, we introduce an address-based identity matching algorithm and a stable slot allocation scheme. The implementation, comprising approximately 2,400 lines of C++ architecture and Python tooling code, has been integrated into the main Faust distribution.
1 0
0
cs.PL 2026-06-12

Grafting function caches cuts robot policy synthesis time 2.3 times

by Saehun Chun, Wonje Choi +3 more

Functional Cache Grafting: Robust and Rapid Code-Policy Synthesis for Embodied Agents

FCGraft retrieves and stitches validated code segments with their caches to build reliable control programs more efficiently than full-promp

Figure from the paper full image
abstract click to expand
Code-writing large language models (CodeLLMs) generate executable code policies for embodied agents by translating natural language goals and environmental constraints into structured control programs. However, policy generation in open-domain embodied environments suffers from two fundamental limitations: (i) delayed decoding caused by repetitive prefill computation over long prompts, and (ii) limited robustness due to fully generative decoding, which often produces API mismatches, missing safety guards, and unstable control logic. To address these limitations, we present FCGraft, a Functional Cache Grafting framework. FCGraft maintains a library of function-level validated code skeletons and their associated prompt-level Transformer key-value (KV) caches, and synthesizes new policies by retrieving relevant functions and grafting their KV caches when a new task is provided. Given retrieved function caches, FCGraft performs cache grafting via stitching, which composes cached function segments into a composite policy, and patching, which locally adapts only the necessary code regions to satisfy task-specific parameters and constraints with minimal additional decoding. By eliminating redundant prefill computation, this approach reduces generation latency, while reusing validated control structures improves robustness over prompt-level caching methods RAGCache, achieving 18.31% higher task success rate and 2.3x faster policy synthesis.
0
0
cs.PL 2026-06-11

nomp framework turns user metadata into domain-optimized GPU code

by Thilina Ratnayaka, Kaushik Kulkarni +9 more

nomp: A Framework for Building Domain Specific Compilers

Pragma model plus runtime aims to reuse proven patterns so productivity rises without losing performance or portability

Figure from the paper full image
abstract click to expand
The low-level GPU programming models (CUDA, HIP, OpenCL, etc.) provide detailed control of the data flow and execution plan of a program in order to extract close-to-metal performance. However, these have a steep learning curve due to the intricacies of their syntax and semantics. This reduces programmer productivity. On the other hand, high-level models (OpenMP, OpenACC, etc.) that serve as abstractions over the low-level models are aimed at improving programmer productivity but achieving performance on-par with the low-level models is a challenge. There are inherent trade-offs between productivity, portability and performance in both approaches and there is no one-size-fits-all solution which achieves all three simultaneously. However, we believe there is room to improve programmer productivity without sacrificing performance and portability by reusing optimization patterns specific to a given domain. To this end, we propose nomp: a framework for building domain specific compilers. nomp consists of a pragma based programming model and a runtime capable of code transformation and generation based on user provided metadata.
0
0
cs.SE 2026-06-10

EMFular generates browser editors that match EMF containment rules

by Susanne Göbel, Ralf Lämmel

Web-Native Graphical EMF Model Editors

The Angular apps handle references and containment exactly like desktop EMF tools but require no server.

Figure from the paper full image
abstract click to expand
Graphical model editing is shifting from desktop applications to web-based tools. We analyze the characteristics of existing frameworks and, based on this analysis, we derive a set of design principles that imply low-effort generation, extensive customization possibilities, and straightforward deployment of the resulting editors. On these grounds, we introduce EMFular, a purely web-based framework for managing EMF models without any backend. The accompanying EMFular generator maps a given Ecore model (an EMF metamodel) to a ready-to-use and ready-to-customize graphical editor. EMFular editors provide 'EMF consistency', that is, they not only support standard modeling operations such as creation, inspection, navigation, editing, and undo/redo, but they also handle containment and inverse references in close alignment with EMF; they also provide interoperability with existing EMF tooling through compatible de-/serialization. A generated editor is an Angular project with designated extension points, which allows developers to customize and extend all aspects of the editor using the expressive power of Angular and its ecosystem, guided by the extension points of EMFular. We evaluate EMFular in terms of editor adequacy (available editing capabilities), adaptability (customization mechanisms and required effort), and robustness of the generation.
0
0
cs.AR 2026-06-10

Zero-copy allocation cuts accelerator data movement by half

by Elam Cohavi, Nicolas Bohm Agostini +4 more

Defeat the Heap: Zero-Copy Data Movement in AXI4MLIR

AXI4MLIR now places buffers directly in DMA-mapped regions and skips the heap staging copy.

Figure from the paper full image
abstract click to expand
As custom hardware accelerators become increasingly central to machine learning workloads, efficient data transfer is critical for maximizing accelerator performance on linear algebra kernels. AXI4MLIR, an extension of the Multi-Level Intermediate Representation (MLIR) compiler framework for automated generation of host-accelerator driver code, incurs significant runtime overhead due to non-zero-copy CPU-accelerator data movement. During transfers from the host to the accelerator, data is copied from heap-allocated memory buffers into contiguous Direct Memory Access (DMA)-mapped buffers. This work identifies this copy as a redundant staging operation and eliminates it through zero-copy data movement. The optimization extends accel, an MLIR dialect introduced by AXI4MLIR, and implements lowering support that allocates buffers directly within DMA-mapped memory, thereby omitting the staging copy. We evaluate the proposed scheme using a configurable matrix-matrix multiplication accelerator and show that the zero-copy optimization reduces main memory data movement by up to 2x, increasing overall accelerator utilization.
0
0
cs.DC 2026-06-10

CRDT stores versioned code to allow partial app updates

by Seppe Wyns, Jim Bauwens +1 more

Dynamic Software Updates using CRDTs

Compatible middleware lets distributed components at mixed versions keep communicating during backwards-incompatible changes.

Figure from the paper full image
abstract click to expand
This paper investigates how Conflict-free Replicated Data Types (CRDTs) can be used for dynamic software updates of distributed applications. We propose to model application updates as a new App CRDT that stores the application code associated with a semantic version, which defines a total order of the code updates. The App CRDT works with an API-compatible message delivery middleware, which allows applications to continue working with partially updated components in the face of backwards-incompatible software updates. We implemented our approach in AmbientTalk, an ambient-oriented programming language designed for distributed systems. We show how this CRDT can be integrated with existing AmbientTalk applications, requiring minimal changes. We also implemented our approach in LuAT, an ambient-oriented programming framework for Lua. This shows that our approach of using CRDTs to replicate code can be generalised to other programming languages.
0
0
cs.PL 2026-06-10

Value iteration replaces optimization in max-policy iteration

by David Monniaux (VERIMAG - IMAG, INS2I-CNRS) +1 more

Max-Policy Iteration, Revisited

For integers and floats, it still terminates and enables precise bounds without widening.

Figure from the paper full image
abstract click to expand
Max-policy iteration is an approach to computing precise numeric program invariants by successive attempts at resolving maximum operators and reduction to mathematical optimization. Mathematical optimization, though, may be expensive. Here, we show, for max-policy iteration on systems of equations over integers as well as over floating point numbers, that mathematical optimization can be replaced by plain value iteration -- which is still guaranteed to terminate. As an application, a precise bound analysis for integer or floating point variables is obtained, avoiding widening operators altogether. We also consider max-policy iteration over the rational numbers, where the right-hand sides are maxima of minima of affine combinations of unknowns. We propose min-policy iteration as an alternative to linear programming for solving the optimization problems posed by max-policy iteration. We prove that max-min policy iteration is guaranteed to return the least solution for bounded systems. We also show how to extend this algorithm to unbounded systems, and how to construct certificates of soundness as well as of optimality of the computed results.
0
0
cs.PL 2026-06-10

ASP encoding rivals ILP for e-graph term extraction

by Ziyi Yang, Ilya Sergey

Answer Set Programming for Egg Extraction and More

Naive approach matches optimized ILP and recovers extra optima on complex instances

Figure from the paper full image
abstract click to expand
Three years ago, Philip Zucker posted an attempt to use answer set programming (ASP) for term extraction from e-graphs Although the task is NP-hard and ASP offers a natural modelling of e-graph terms, the initial attempt did not yield convincing results. From the aspect of practical ASP users, we first pinpoint the way to make ASP work and work well on the task of e-graph extraction. The initial results show the na\"ive ASP encoding is comparable on efficiency to the well-optimised ILP-based exact DAG extraction in the extraction-gym, and find several extra optimal extraction on the complex instances. This leads us to a further agenda: with the "better together of egg+Datalog", is there a better "better together" by having ASP as a more powerful Datalog? We discuss the potential benefit from each other.
0
0
cs.RO 2026-06-09

Graphical tool replaces XML editing for ROS launch files

by Kate Sanborn, Tanuj Kenchannavar +2 more

Modeling Components and Connections in Cyber-Physical Systems

Developers draw nodes, publishers and links with automatic validation instead of writing text configurations.

abstract click to expand
Text based configuration files for cyber-physical systems show the hierarchy of component modules well but often hide the details of connections and interfaces between modules. A model-based visual approach to these configuration files can better capture this information. The XML structure of Robot Operating System (ROS) launch files can be improved using a modeling approach. This paper presents ROSLaunchVisual, a model-integrated environment built on WebGME for designing, visualizing, and managing ROS launch files. The tool raises the level of abstraction by allowing developers to create and modify launch files using a graphical interface that represents nodes, publishers, subscribers, and arguments as interconnected components. The tool provides a dynamic system analysis that can then be used in the static development and analysis of new and existing launch files. ROSLaunchVisual incorporates features such as metamodel-driven validation, automatic import/export of launch files, and visual communication mapping. Plugins further enhance functionality by updating libraries, checking for semantic errors, and managing remaps. By making launch file creation more intuitive and less error-prone, ROSLaunchVisual improves development efficiency and system understanding, especially in collaborative or large-scale robotics projects.
0
0
cs.LO 2026-06-09

Intersection types characterize termination for effects and handlers

by Ugo Dal Lago, Taro Sekiyama +1 more

When Types Intersect and Effects Get Handled

The system also converts reachability into type inference and produces a decidable simple type system.

Figure from the paper full image
abstract click to expand
We introduce a novel intersection type system for a $\lambda$-calculus with algebraic effects and handlers. The system, inherently behavioral in nature, enjoys the classical properties of intersection type systems, in particular subject reduction and expansion. It thus characterizes the set of terms whose evaluation process terminates and, at the same time, allows reducing the reachability problem to type inference. This new system, the first with these features for a calculus with handlers, induces a system of simple types which, although not guaranteeing termination, is type sound and admits a decidable HOMC problem, unlike similar type systems like Dal Lago and Ghyselen's HEPCF.
0

browse all of cs.PL → full archive · search · sub-categories