https://arxiv.org/api/+fHufQldx+tGRdXw/nbwITclSuE 2026-06-23T18:52:20Z 9934 1080 15 http://arxiv.org/abs/2510.11420v1 2025-10-13T13:55:54Z

We introduce the Hierarchical Unified Graph Representation (HUGR): a novel graph based intermediate representation for mixed quantum-classical programs. HUGR's design features high expressivity and extensibility to capture the capabilities of near-term and forthcoming quantum computing devices, as well as new and evolving abstractions from novel quantum programming paradigms. The graph based structure is machine-friendly and supports powerful pattern matching based compilation techniques. Inspired by MLIR, HUGR's extensibility further allows compilation tooling to reason about programs at multiple levels of abstraction, lowering smoothly between them. Safety guarantees in the structure including strict, static typing and linear quantum types allow rapid development of compilation tooling without fear of program invalidation. A full specification of HUGR and reference implementation are open-source and available online.

2025-10-13T13:55:54Z 8 pages, extended abstract submitted to PlanQC25 Mark Koch Agustín Borgna Seyon Sivarajah Alan Lawrence Alec Edgington Douglas Wilson Craig Roy Luca Mondada Lukas Heidemann Ross Duncan http://arxiv.org/abs/2305.14019v4 2025-10-13T11:16:34Z

As large language models (LLMs) like ChatGPT exhibited unprecedented machine intelligence, it also shows great performance in assisting hardware engineers to realize higher-efficiency logic design via natural language interaction. To estimate the potential of the hardware design process assisted by LLMs, this work attempts to demonstrate an automated design environment that explores LLMs to generate hardware logic designs from natural language specifications. To realize a more accessible and efficient chip development flow, we present a scalable four-stage zero-code logic design framework based on LLMs without retraining or finetuning. At first, the demo, ChipGPT, begins by generating prompts for the LLM, which then produces initial Verilog programs. Second, an output manager corrects and optimizes these programs before collecting them into the final design space. Eventually, ChipGPT will search through this space to select the optimal design under the target metrics. The evaluation sheds some light on whether LLMs can generate correct and complete hardware logic designs described by natural language for some specifications. It is shown that ChipGPT improves programmability, and controllability, and shows broader design optimization space compared to prior work and native LLMs alone.

2023-05-23T12:54:02Z Accepted by 2023 NeurIPS SysML Workshop, retitled to "Improving Large Language Model Hardware Generating Quality through Post-LLM Search" Kaiyan Chang Ying Wang Haimeng Ren Mengdi Wang Shengwen Liang Yinhe Han Huawei Li Xiaowei Li http://arxiv.org/abs/2505.04500v2 2025-10-13T09:55:38Z

VeriFast is one of the leading tools for semi-automated modular formal program verification. A central feature of VeriFast is its support for higher-order ghost code, which enables its support for expressively specifying fine-grained concurrent modules, without the need for the later modality. We present the first formalization and soundness proof for this aspect of VeriFast's logic, and we compare it both to Iris, a state-of-the-art logic for fine-grained concurrency which features the later modality, as well as to some recent proposals for Iris-like reasoning without the later modality.

2025-05-07T15:21:02Z 10 pages, 8 figures Bart Jacobs http://arxiv.org/abs/2510.11199v1 2025-10-13T09:31:16Z

These are the contributed papers presented at the 20th International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2025), at Birmingham, UK on 19 July as a satellite event of the FSCD conference. The program committee for this edition of LFMTP was chaired by Kaustuv Chaudhuri and Daniele Nantes-Sobrinho. More information about LFMTP can be found on https://lfmtp.org.

2025-10-13T09:31:16Z EPTCS 431, 2025 Kaustuv Chaudhuri Inria, France Daniele Nantes-Sobrinho Imperial College, UK 10.4204/EPTCS.431 http://arxiv.org/abs/2508.10068v2 2025-10-13T07:16:49Z

Despite Retrieval-Augmented Generation improving code completion, traditional retrieval methods struggle with information redundancy and a lack of diversity within limited context windows. To solve this, we propose a resource-optimized retrieval augmentation method, SaraCoder. It maximizes information diversity and representativeness in a limited context window, significantly boosting the accuracy and reliability of repository-level code completion. Its core Hierarchical Feature Optimization module systematically refines candidates by distilling deep semantic relationships, pruning exact duplicates, assessing structural similarity with a novel graph-based metric that weighs edits by their topological importance, and reranking results to maximize both relevance and diversity. Furthermore, an External-Aware Identifier Disambiguator module accurately resolves cross-file symbol ambiguity via dependency analysis. Extensive experiments on the challenging CrossCodeEval and RepoEval-Updated benchmarks demonstrate that SaraCoder outperforms existing baselines across multiple programming languages and models. Our work proves that systematically refining retrieval results across multiple dimensions provides a new paradigm for building more accurate and resource-optimized repository-level code completion systems.

2025-08-13T11:56:05Z Xiaohan Chen Zhongying Pan Quan Feng Yu Tian Shuqun Yang Mengru Wang Lina Gong Yuxia Geng Piji Li Xiang Chen http://arxiv.org/abs/2510.11007v1 2025-10-13T04:55:40Z

We introduce a string-interval abstract domain, where string intervals are characterized by systems of word equations (encoding lower bounds on string values) and word disequalities (encoding upper bounds). Building upon the lattice structure of string intervals, we define an abstract string object as a reduced product on a string property semilattice, determined by length-non-increasing morphisms. We consider several reduction strategies for abstract string objects and show that upon these strategies the string object domain forms a lattice. We define basic abstract string operations on the domain, aiming to minimize computational overheads on the reduction, and show how the domain can be used to analyse properties of JavaScript string manipulating programs.

2025-10-13T04:55:40Z Antonina Nepeivoda Ilya Afanasyev http://arxiv.org/abs/2510.11759v1 2025-10-13T02:02:36Z

Compiler optimization is crucial for enhancing program performance by transforming the sequence of optimization passes while maintaining correctness. Despite the promising potential of large language models (LLMs)-based agent for software optimization, automating compiler optimization remains challenging due to: (1) semantic misalignment between abstract program representations and concrete optimization passes, (2) inefficient interaction mechanisms between agents and compiler environments, and (3) reward sparsity from the extensive decision-making process within large optimization spaces. This paper introduces \textbf{AwareCompiler}, an agentic framework for compiler optimization that addresses these challenges through three key innovations: structured knowledge integration and dataset construction, knowledge-driven adaptive pass generation, and data-driven hybrid training pipeline. Experimental results on standard benchmarks demonstrate that AwareCompiler significantly outperforms existing baselines in both performance and efficiency, highlighting the effectiveness of our synergistic knowledge-data-driven approach. Our code is publicly available at https://github.com/LHY-24/AwareCompiler.

2025-10-13T02:02:36Z Hongyu Lin Haolin Pan Haoran Luo Yuchen Li Kaichun Yao Libo Zhang Mingjie Xing Yanjun Wu http://arxiv.org/abs/2510.10531v1 2025-10-12T10:12:16Z

Remote Direct Memory Access (RDMA) is a memory technology that allows remote devices to directly write to and read from each other's memory, bypassing components such as the CPU and operating system. This enables low-latency high-throughput networking, as required for many modern data centres, HPC applications and AI/ML workloads. However, baseline RDMA comprises a highly permissive weak memory model that is difficult to use in practice and has only recently been formalised. In this paper, we introduce the Library of Composable Objects (LOCO), a formally verified library for building multi-node objects on RDMA, filling the gap between shared memory and distributed system programming. LOCO objects are well-encapsulated and take advantage of the strong locality and the weak consistency characteristics of RDMA. They have performance comparable to custom RDMA systems (e.g. distributed maps), but with a far simpler programming model amenable to formal proofs of correctness. To support verification, we develop a novel modular declarative verification framework, called Mowgli, that is flexible enough to model multinode objects and is independent of a memory consistency model. We instantiate Mowgli with the RDMA memory model, and use it to verify correctness of LOCO libraries.

2025-10-12T10:12:16Z Guillaume Ambal George Hodgkins Mark Madler Gregory Chockler Brijesh Dongol Joseph Izraelevitz Azalea Raad Viktor Vafeiadis http://arxiv.org/abs/2510.10517v1 2025-10-12T09:29:24Z

Code runtime optimization-the task of rewriting a given code to a faster one-remains challenging, as it requires reasoning about performance trade-offs involving algorithmic and structural choices. Recent approaches employ code-LLMs with slow-fast code pairs provided as optimization guidance, but such pair-based methods obscure the causal factors of performance gains and often lead to superficial pattern imitation rather than genuine performance reasoning. We introduce ECO, a performance-aware prompting framework for code optimization. ECO first distills runtime optimization instructions (ROIs) from reference slow-fast code pairs; Each ROI describes root causes of inefficiency and the rationales that drive performance improvements. For a given input code, ECO in parallel employs (i) a symbolic advisor to produce a bottleneck diagnosis tailored to the code, and (ii) an ROI retriever to return related ROIs. These two outputs are then composed into a performance-aware prompt, providing actionable guidance for code-LLMs. ECO's prompts are model-agnostic, require no fine-tuning, and can be easily prepended to any code-LLM prompt. Our empirical studies highlight that ECO prompting significantly improves code-LLMs' ability to generate efficient code, achieving speedups of up to 7.81x while minimizing correctness loss.

2025-10-12T09:29:24Z Su-Hyeon Kim Joonghyuk Hahn Sooyoung Cha Yo-Sub Han http://arxiv.org/abs/2503.03207v3 2025-10-12T02:22:31Z

Several software systems are polyglot; that is, they comprise programs implemented in a combination of programming languages. Verifiers that directly run on mainstream programming languages are currently customized for single languages. Thus, to verify polyglot systems, one usually translates them into a common verification language or formalism on which the verifier runs. In this paper, we present an alternative approach, PolyVer, which employs abstraction, compositional reasoning, and synthesis to directly perform polyglot verification. PolyVer constructs a formal model of the original polyglot system as a transition system where the update functions associated with transitions are implemented in target languages such as C or Rust. To perform verification, PolyVer then connects a model checker for transition systems with language-specific verifiers (e.g., for C or Rust) using pre/post-condition contracts for the update functions. These contracts are automatically generated by synthesis oracles based on syntax-guided synthesis or large language models (LLMs), and checked by the language-specific verifiers. The contracts form abstractions of the update functions using which the model checker verifies the overall system-level property on the polyglot system model. PolyVer iterates between counterexample-guided abstraction-refinement (CEGAR) and counterexample-guided inductive synthesis (CEGIS) until the property is verified or a true system-level counterexample is found. We demonstrate the utility of PolyVer for verifying programs in the Lingua Franca polyglot language using the UCLID5 model checker connected with the CBMC and Kani verifiers for C and Rust respectively.

2025-03-05T05:52:33Z Proceedings of the 25th Conference on Formal Methods in Computer-Aided Design (FMCAD 2025) Pei-Wei Chen Shaokai Lin Adwait Godbole Ramneet Singh Elizabeth Polgreen Edward A. Lee Sanjit A. Seshia 10.34727/2025/isbn.978-3-85448-084-6_10 http://arxiv.org/abs/2510.11751v1 2025-10-12T01:07:25Z

Correct concurrent behaviour is important in understanding how components will act within certain conditions. In this work. we analyse the behaviour of shared communicating channels within a coorporatively scheduled runtime. We use the refinement checking and modelling tool FDR to develop both specifications of how such shared channels should behave and models of the implementations of these channels in the cooperatively scheduled language ProcessJ. Our results demonstrate that although we can certainly implement the correct behaviour of such channels, the outcome is dependant on having adequate resources available to execute all processes involved. We conclude that modelling the runtime environment of concurrent components is necessary to ensure components behave as specified in the real world.

2025-10-12T01:07:25Z Jan Pedersen Kevin Chalmers http://arxiv.org/abs/2510.10219v1 2025-10-11T13:52:48Z

Memory allocators hide beneath nearly every application stack, yet their performance footprint extends far beyond their code size. Even small inefficiencies in the allocators ripple through caches and the rest of the memory hierarchy, collectively imposing what operators often call a "datacenter tax". At hyperscale, even a 1% improvement in allocator efficiency can unlock millions of dollars in savings and measurable reductions in datacenter energy consumption. Modern memory allocators are designed to optimize allocation speed and memory fragmentation in multi-threaded environments, relying on complex metadata and control logic to achieve high performance. However, the overhead introduced by this complexity prompts a reevaluation of allocator design. Notably, such overhead can be avoided in single-threaded scenarios, which continue to be widely used across diverse application domains. In this paper, we introduce Exgen-Malloc, a memory allocator purpose-built for single-threaded applications. By specializing for single-threaded execution, Exgen-Malloc eliminates unnecessary metadata, simplifies the control flow, thereby reducing overhead and improving allocation efficiency. Its core design features include a centralized heap, a single free-block list, and a balanced strategy for memory commitment and relocation. Additionally, Exgen-Malloc incorporates design principles in modern multi-threaded allocators, which do not exist in legacy single-threaded allocators such as dlmalloc. We evaluate Exgen-Malloc on two Intel Xeon platforms. Across both systems, Exgen-Malloc achieves a speedup of 1.17x, 1.10x, and 1.93x over dlmalloc on SPEC CPU2017, redis-benchmark, and mimalloc-bench, respectively. In addition to performance, Exgen-Malloc achieves 6.2%, 0.1%, and 25.2% memory savings over mimalloc on SPEC CPU2017, redis-benchmark, and mimalloc-bench, respectively.

2025-10-11T13:52:48Z Ruihao Li Lizy K. John Neeraja J. Yadwadkar http://arxiv.org/abs/2510.10015v1 2025-10-11T04:41:43Z

Program safety (i.e., absence of undefined behaviors) is critical for correct operation of computer systems. It is usually verified at the source level (e.g., by separation logics) and preserved to the target by verified compilers (e.g., CompCert), thereby achieving end-to-end verification of safety. However, modern safe programming languages like Rust pose new problems in achieving end-to-end safety. Because not all functionalities can be implemented in the safe language, mixing safe and unsafe modules is needed. Therefore, verified compilation must preserve a modular notion of safety which can be composed at the target level. Furthermore, certain classes of errors (e.g., memory errors) are automatically excluded by verifying compilation (e.g., borrow checking) for modules written in safe languages. As a result, verified compilation needs to cooperate with verifying compilation to ensure end-to-end safety. To address the above problems, we propose a modular and generic definition of safety called open safety based on program semantics described as open labeled transition systems (LTS). Open safety is composable at the boundary of modules and can be modularly preserved by verified compositional compilation. Those properties enable separate verification of safety for heterogeneous modules and composition of the safety results at the target level. Open safety can be generalized to partial safety (i.e., only a certain class of errors can occur). By this we formalized the correctness of verifying compilation as derivation of total safety from partial safety. We demonstrate how our framework can combine verified and verifying compilation by developing a verified compiler for an ownership language (called Owlang) inspired by Rust. We evaluate our approach on the compositional safety verification using a hash map implemented by Owlang and C.

2025-10-11T04:41:43Z Jinhua Wu Yuting Wang Liukun Yu Linglong Meng http://arxiv.org/abs/2510.09932v1 2025-10-11T00:11:34Z

Tensor compilers play a key role in enabling high-performance implementations of deep learning workloads. These compilers rely on existing CPU and GPU code generation backends to generate device-specific code. Recently, many tensor accelerators (neural processing units) have been proposed to further accelerate these workloads. Compared to commodity hardware, however, most of the proposed tensor accelerators do not have compiler backends with code generation support. Moreover, the accelerator designs are subject to fast iteration cycles, making it difficult to manually develop compiler backends similar to commodity hardware platforms. Therefore, to increase adoption and enable faster software development cycles for novel tensor accelerator designs, we need to make the compiler backend construction process more agile. To address this gap, we introduce ACT, a compiler backend generator that automatically generates compiler backends for tensor accelerators, given just the instruction set architecture (ISA) descriptions. We first formally specify the compiler backend generation problem that introduces a novel specification for describing tensor accelerator ISAs. Next, we design ACT such that it supports user-programmable memories and complex parameterized instructions that are prevalent in tensor accelerators. ACT uses a novel parameterized equality saturation-based instruction selection phase and a constraint programming-based memory allocation phase. We prove that compiler backends generated by ACT are sound and complete. Finally, we generate compiler backends for three accelerator platforms from industry and academia, and show that they match or outperform code written using hand-optimized kernel libraries while maintaining low compilation overheads.

2025-10-11T00:11:34Z Devansh Jain Akash Pardeshi Marco Frigo Krut Patel Kaustubh Khulbe Jai Arora Charith Mendis http://arxiv.org/abs/2510.09591v1 2025-10-10T17:49:39Z

All widely used and useful programming languages have a common problem. They restrict entry on the basis of knowledge of the English language. The lack of knowledge of English poses a major hurdle to many newcomers who do not have the resources, in terms of time and money, to learn the English language. Studies show that people learn better in their own language. Therefore, we propose a language transpiler built on top of the Python programming language, called UniversalPython, which allows one to write Python in their own human language. We demonstrate the ability to create an "Urdu Python" with this transpiler. In the future, we aim to scale the language to encapsulate more human languages to increase the availability of programming. The source code for this transpiler is open-source, and available at https://github.com/universalpython/universalpython

2025-10-10T17:49:39Z For project homepage, see https://universalpython.github.io/ Saad Ahmed Bazaz Mirza Omer Beg