https://arxiv.org/api/tAroALuxqopqdixC0ZKw3+DF/kI 2026-06-28T15:45:14Z 9951 1605 15 http://arxiv.org/abs/2307.15641v3 2025-05-06T18:39:37Z

Thanks to the rapid progress and growing complexity of quantum algorithms, correctness of quantum programs has become a major concern. Pioneering research over the past years has proposed various approaches to formally verify quantum programs using proof systems such as quantum Hoare logic. All these prior approaches are post-hoc: one first implements a program and only then verifies its correctness. Here we propose Quantum Correctness by Construction (QbC): an approach to constructing quantum programs from their specification in a way that ensures correctness. We use pre- and postconditions to specify program properties, and propose sound and complete refinement rules for constructing programs in a quantum while language from their specification. We validate QbC by constructing quantum programs for idiomatic problems and patterns. We find that the approach naturally suggests how to derive program details, highlighting key design choices along the way. As such, we believe that QbC can play a role in supporting the design and taxonomization of quantum algorithms and software.

2023-07-28T16:00:57Z v3. 43 pages, latest author version, to appear at OOPSLA 2025 Proc. ACM Program. Lang. 9, OOPSLA1, Article 99 (April 2025) Anurudh Peduri Ina Schaefer Michael Walter http://arxiv.org/abs/2504.06789v2 2025-05-06T12:37:24Z

We study the relationship between partial map classifiers, Sierpiński cones, and axioms for synthetic higher categories and domains within univalent foundations. In particular, we show that synthetic $\infty$-categories are closed under partial map classifiers assuming Phoa's principle, and we isolate a new reflective subuniverse of types within which the Sierpiński cone (a lax colimit) can be computed as a partial map classifier by strengthening the Segal condition.

2025-04-09T11:27:54Z To appear in to LICS 2025. Main result updated to omit unnecessary side condition (boundary separation) Leoni Pugh Jonathan Sterling http://arxiv.org/abs/2505.02883v1 2025-05-05T12:44:13Z

System design automation aims to manage the design of embedded systems with ever-increasing complexity. To the success of system design automation, there is still a lack of systematic and formal design process because an entire design process, from a system's specification to its implementation, has to deal with inherent concerns about the systems' different aspects and, consequently, inherent semantic gaps. These gaps make it hard for a design process to be traceable or transparent. Particularly, guaranteeing the correctness of produced implementations becomes the main challenge for a system design process. SynQ (Synchronous system design with Quantitative types) is an embedded domain specification language (EDSL) targeting the design of systems obeying the perfect synchrony hypothesis. SynQ is based on a component-based design framework and, by design, facilitates semantic coherency by leveraging the quantitative type theory (QTT) and language embedding. SynQ enables a semantically coherent design process, including formal specification and verification, modelling, simulation and code generation. This paper presents SynQ and its underlying formalism and demonstrates its features and potential for semantically coherent system design through a case study.

2025-05-05T12:44:13Z 45 pages, 15 figures Rui Chen Ingo Sander http://arxiv.org/abs/2505.02493v1 2025-05-05T09:21:58Z

The decentralized and unregulated nature of cryptocurrencies, combined with their monetary value, has made them a vehicle for various illicit activities. One such activity is cryptojacking, an attack that uses stolen computing resources to mine cryptocurrencies without consent for profit. In-browser cryptojacking malware exploits high-performance web technologies like WebAssembly to mine cryptocurrencies directly within the browser without file downloads. Although existing methods for cryptomining detection report high accuracy and low overhead, they are often susceptible to various forms of obfuscation, and due to the limited variety of cryptomining scripts in the wild, standard code obfuscation methods present a natural and appealing solution to avoid detection. To address these limitations, we propose using instruction-level data-flow graphs to detect cryptomining behavior. Data-flow graphs offer detailed structural insights into a program's computations, making them suitable for characterizing proof-of-work algorithms, but they can be difficult to analyze due to their large size and susceptibility to noise and fragmentation under obfuscation. We present two techniques to simplify and compare data-flow graphs: (1) a graph simplification algorithm to reduce the computational burden of processing large and granular data-flow graphs while preserving local substructures; and (2) a subgraph similarity measure, the n-fragment inclusion score, based on fragment inclusion that is robust against noise and obfuscation. Using data-flow graphs as computation fingerprints, our detection framework PoT (Proof-of-Theft) was able to achieve high detection accuracy against standard obfuscations, outperforming existing detection methods. Moreover, PoT uses generic data-flow properties that can be applied to other platforms more susceptible to cryptojacking such as servers and data centers.

2025-05-05T09:21:58Z Tanapoom Sermchaiwong Jiasi Shen http://arxiv.org/abs/2505.02346v1 2025-05-05T04:01:56Z

Python is a popular programming language known for its ease of learning and extensive libraries. However, concerns about performance and energy consumption have led to the development of compilers to enhance Python code efficiency. Despite the proven benefits of existing compilers on the efficiency of Python code, there is limited analysis comparing their performance and energy efficiency, particularly considering code characteristics and factors like CPU frequency and core count. Our study investigates how compilation impacts the performance and energy consumption of Python code, using seven benchmarks compiled with eight different tools: PyPy, Numba, Nuitka, Mypyc, Codon, Cython, Pyston-lite, and the experimental Python 3.13 version, compared to CPython. The benchmarks are single-threaded and executed on an NUC and a server, measuring energy usage, execution time, memory usage, and Last-Level Cache (LLC) miss rates at a fixed frequency and on a single core. The results show that compilation can significantly enhance execution time, energy and memory usage, with Codon, PyPy, and Numba achieving over 90\% speed and energy improvements. Nuitka optimizes memory usage consistently on both testbeds. The impact of compilation on LLC miss rate is not clear since it varies considerably across benchmarks for each compiler. Our study is important for researchers and practitioners focused on improving Python code performance and energy efficiency. We outline future research directions, such as exploring caching effects on energy usage. Our findings help practitioners choose the best compiler based on their efficiency benefits and accessibility.

2025-05-05T04:01:56Z Vincenzo Stoico Andrei Calin Dragomir Patricia Lago http://arxiv.org/abs/2407.01638v2 2025-05-04T17:21:20Z

This paper addresses the problem of providing a novel approach to sourcing significant training data for LLMs focused on science and engineering. In particular, a crucial challenge is sourcing parallel scientific codes in the ranges of millions to billions of codes. To tackle this problem, we propose an automated pipeline framework called LASSI, designed to translate between parallel programming languages by bootstrapping existing closed- or open-source LLMs. LASSI incorporates autonomous enhancement through self-correcting loops where errors encountered during the compilation and execution of generated code are fed back to the LLM through guided prompting for debugging and refactoring. We highlight the bi-directional translation of existing GPU benchmarks between OpenMP target offload and CUDA to validate LASSI. The results of evaluating LASSI with different application codes across four LLMs demonstrate the effectiveness of LASSI for generating executable parallel codes, with 80% of OpenMP to CUDA translations and 85% of CUDA to OpenMP translations producing the expected output. We also observe approximately 78% of OpenMP to CUDA translations and 62% of CUDA to OpenMP translations execute within 10% of or at a faster runtime than the original benchmark code in the same language.

2024-06-30T19:36:04Z 8 pages, 1 figure, 7 tables 2024 IEEE International Conference on Cluster Computing Workshops (CLUSTER Workshops), pp. 136-143 Matthew T. Dearing Yiheng Tao Xingfu Wu Zhiling Lan Valerie Taylor 10.1109/CLUSTERWorkshops61563.2024.00029 http://arxiv.org/abs/2505.02146v1 2025-05-04T15:14:27Z

Heterogeneous deep learning systems (DLS) such as GPUs and ASICs have been widely deployed in industrial data centers, which requires to develop multiple low-level tensor programs for different platforms. An attractive solution to relieve the programming burden is to transcompile the legacy code of one platform to others. However, current transcompilation techniques struggle with either tremendous manual efforts or functional incorrectness, rendering "Write Once, Run Anywhere" of tensor programs an open question. We propose a novel transcompiler, i.e., QiMeng-Xpiler, for automatically translating tensor programs across DLS via both large language models (LLMs) and symbolic program synthesis, i.e., neural-symbolic synthesis. The key insight is leveraging the powerful code generation ability of LLM to make costly search-based symbolic synthesis computationally tractable. Concretely, we propose multiple LLM-assisted compilation passes via pre-defined meta-prompts for program transformation. During each program transformation, efficient symbolic program synthesis is employed to repair incorrect code snippets with a limited scale. To attain high performance, we propose a hierarchical auto-tuning approach to systematically explore both the parameters and sequences of transformation passes. Experiments on 4 DLS with distinct programming interfaces, i.e., Intel DL Boost with VNNI, NVIDIA GPU with CUDA, AMD MI with HIP, and Cambricon MLU with BANG, demonstrate that QiMeng-Xpiler correctly translates different tensor programs at the accuracy of 95% on average, and the performance of translated programs achieves up to 2.0x over vendor-provided manually-optimized libraries. As a result, the programming productivity of DLS is improved by up to 96.0x via transcompiling legacy tensor programs.

2025-05-04T15:14:27Z Accepted to OSDI 2025 Shouyang Dong Yuanbo Wen Jun Bi Di Huang Jiaming Guo Jianxing Xu Ruibai Xu Xinkai Song Yifan Hao Xuehai Zhou Tianshi Chen Qi Guo Yunji Chen http://arxiv.org/abs/2505.01901v1 2025-05-03T19:16:23Z

This paper examines the philosophical relationship between Thomas Kuhn's concept of scientific paradigms and the programming paradigm concept in computing that was introduced by Floyd in his 1978 Turing Award lecture. Through critical analysis of both Kuhn's original framework and its application in computing, we argue that the contemporary usage of `programming paradigms' represents a significant departure from Kuhn's philosophical concept. We demonstrate that while Floyd explicitly attributed this term to Kuhn's work, his usage fundamentally altered the concept's meaning. We argue that this divergence necessitates a critical reassessment of the term's usage in computing discourse.

2025-05-03T19:16:23Z Peyman M. Kiasari http://arxiv.org/abs/2505.01894v1 2025-05-03T19:08:00Z

Assurance cases (ACs) are prepared to argue that a system has satisfied critical quality attributes. Many methods exist to assess confidence in ACs, including quantitative methods that represent confidence numerically. While quantitative methods are attractive in principle, existing methods suffer from issues related to interpretation, subjectivity, scalability, dialectic reasoning, and trustworthiness, which have limited their adoption. This paper introduces Certus, a domain specific language for quantitative confidence assessment. In Certus, users describe their confidence with fuzzy sets, which allow them to represent their judgment using vague, but linguistically meaningful terminology. Certus includes syntax to specify confidence propagation using expressions that can be easily inspected by users. To demonstrate the concept of the language, Certus is applied to a worked example from the automotive domain.

2025-05-03T19:08:00Z Preprint. Submitted to SASSUR'25 Simon Diemert Jens H. Weber http://arxiv.org/abs/2505.01637v1 2025-05-03T00:14:31Z

High-throughput neural network inference requires coordinating many optimization decisions, including parallel tiling, microkernel selection, and data layout. The product of these decisions forms a search space of programs which is typically intractably large. Existing approaches (e.g., auto-schedulers) often address this problem by sampling this space heuristically. In contrast, we introduce a dynamic-programming-based approach to explore more of the search space by iteratively decomposing large program specifications into smaller specifications reachable from a set of rewrites, then composing a final program from each rewrite that minimizes an affine cost model. To reduce memory requirements, we employ a novel memoization table representation, which indexes specifications by coordinates in $Z_{\geq 0}$ and compresses identical, adjacent solutions. This approach can visit a much larger set of programs than prior work. To evaluate the approach, we developed Morello, a compiler which lowers specifications roughly equivalent to a few-node XLA computation graph to x86. Notably, we found that an affine cost model is sufficient to surface high-throughput programs. For example, Morello synthesized a collection of matrix multiplication benchmarks targeting a Zen 1 CPU, including a 1x2048x16384, bfloat16-to-float32 vector-matrix multiply, which was integrated into Google's gemma.cpp.

2025-05-03T00:14:31Z 13 pages, 2 figures Samuel J. Kaufman René Just Rastislav Bodik http://arxiv.org/abs/2505.01536v1 2025-05-02T18:51:52Z

Disassembly is the first step of a variety of binary analysis and transformation techniques, such as reverse engineering, or binary rewriting. Recent disassembly approaches consist of three phases: an exploration phase, that overapproximates the binary's code; an analysis phase, that assigns weights to candidate instructions or basic blocks; and a conflict resolution phase, that downselects the final set of instructions. We present a disassembly algorithm that generalizes this pattern for a wide range of architectures, namely x86, x64, arm32, and aarch64. Our algorithm presents a novel conflict resolution method that reduces disassembly to weighted interval scheduling.

2025-05-02T18:51:52Z Accepted for publication at the 46th IEEE Symposium on Security and Privacy Antonio Flores-Montoya Junghee Lim Adam Seitz Akshay Sood Edward Raff James Holt http://arxiv.org/abs/2505.01282v1 2025-05-02T13:58:42Z

Solidity is the predominant programming language for blockchain-based smart contracts, and its characteristics pose significant challenges for code analysis and maintenance. Traditional software analysis approaches, while effective for conventional programming languages, often fail to address Solidity-specific features such as gas optimization and security constraints. This paper introduces micro-patterns - recurring, small-scale design structures that capture key behavioral and structural peculiarities specific to a language - for Solidity language and demonstrates their value in understanding smart contract development practices. We identified 18 distinct micro-patterns organized in five categories (Security, Functional, Optimization, Interaction, and Feedback), detailing their characteristics to enable automated detection. To validate this proposal, we analyzed a dataset of 23258 smart contracts from five popular blockchains (Ethereum, Polygon, Arbitrum, Fantom and Optimism). Our analysis reveals widespread adoption of micro-patterns, with 99% of contracts implementing at least one pattern and an average of 2.76 patterns per contract. The Storage Saver pattern showed the highest adoption (84.62% mean coverage), while security patterns demonstrated platform-specific adoption rates. Statistical analysis revealed significant platform-specific differences in pattern adoption, particularly in Borrower, Implementer, and Storage Optimization patterns.

2025-05-02T13:58:42Z Luca Ruschioni Robert Shuttleworth Rumyana Neykova Barbara Re Giuseppe Destefanis http://arxiv.org/abs/2505.00963v1 2025-05-02T02:41:02Z

Formal verification is a rigorous approach that can provably ensure the quality of neural networks, and to date, Branch and Bound (BaB) is the state-of-the-art that performs verification by splitting the problem as needed and applying off-the-shelf verifiers to sub-problems for improved performance. However, existing BaB may not be efficient, due to its naive way of exploring the space of sub-problems that ignores the \emph{importance} of different sub-problems. To bridge this gap, we first introduce a notion of ``importance'' that reflects how likely a counterexample can be found with a sub-problem, and then we devise a novel verification approach, called ABONN, that explores the sub-problem space of BaB adaptively, in a Monte-Carlo tree search (MCTS) style. The exploration is guided by the ``importance'' of different sub-problems, so it favors the sub-problems that are more likely to find counterexamples. As soon as it finds a counterexample, it can immediately terminate; even though it cannot find, after visiting all the sub-problems, it can still manage to verify the problem. We evaluate ABONN with 552 verification problems from commonly-used datasets and neural network models, and compare it with the state-of-the-art verifiers as baseline approaches. Experimental evaluation shows that ABONN demonstrates speedups of up to $15.2\times$ on MNIST and $24.7\times$ on CIFAR-10. We further study the influences of hyperparameters to the performance of ABONN, and the effectiveness of our adaptive tree exploration.

2025-05-02T02:41:02Z 7 pages, 6 figures Kota Fukuda Guanqin Zhang Zhenya Zhang Yulei Sui Jianjun Zhao http://arxiv.org/abs/2505.07834v1 2025-05-02T00:33:00Z

We introduce ai.txt, a novel domain-specific language (DSL) designed to explicitly regulate interactions between AI models, agents, and web content, addressing critical limitations of the widely adopted robots.txt standard. As AI increasingly engages with online materials for tasks such as training, summarization, and content modification, existing regulatory methods lack the necessary granularity and semantic expressiveness to ensure ethical and legal compliance. ai.txt extends traditional URL-based access controls by enabling precise element-level regulations and incorporating natural language instructions interpretable by AI systems. To facilitate practical deployment, we provide an integrated development environment with code autocompletion and automatic XML generation. Furthermore, we propose two compliance mechanisms: XML-based programmatic enforcement and natural language prompt integration, and demonstrate their effectiveness through preliminary experiments and case studies. Our approach aims to aid the governance of AI-Internet interactions, promoting responsible AI use in digital ecosystems.

2025-05-02T00:33:00Z Yuekang Li Wei Song Bangshuo Zhu Dong Gong Yi Liu Gelei Deng Chunyang Chen Lei Ma Jun Sun Toby Walsh Jingling Xue http://arxiv.org/abs/2406.00602v2 2025-05-01T02:34:03Z

Large Language Models (LLMs) have demonstrated promising capabilities for code generation. While existing benchmarks evaluate the correctness and efficiency of LLM-generated code, the potential linguistic bias - where code quality varies based on the natural language used to describe programming tasks - remains underexplored. In this paper, we aim to investigate this linguistic bias through the lens of English and Chinese. To facilitate our investigation, we present a unified evaluation framework comprising a curated dataset of 52 Python programming questions with parallel bilingual task descriptions, automated correctness verification, and efficiency quantification tools based on runtime complexity estimation. Based on this framework, we conduct the first empirical study towards the linguistic bias in LLM-generated code on eight popular LCGMs, as well as GPT-3.5-Turbo and GPT-4. We observe that these LCGM-generated code show different correctness on an average of 12% bilingual programming tasks, where 39% also exhibits diverse efficiency. Our findings indicate that LLMs commonly exhibit linguistic bias for code generation.

2024-06-02T03:22:30Z Weipeng Jiang Xuanqi Gao Juan Zhai Shiqing Ma Xiaoyu Zhang Ziyan Lei Chao Shen