https://arxiv.org/api/vknQWOgJDbgBXAAZsBUJZElsegU 2026-06-29T00:44:39Z 9951 1725 15 http://arxiv.org/abs/2307.11128v2 2025-03-19T20:02:42Z

The challenging deployment of compute-intensive applications from domains such as Artificial Intelligence (AI) and Digital Signal Processing (DSP), forces the community of computing systems to explore new design approaches. Approximate Computing appears as an emerging solution, allowing to tune the quality of results in the design of a system in order to improve the energy efficiency and/or performance. This radical paradigm shift has attracted interest from both academia and industry, resulting in significant research on approximation techniques and methodologies at different design layers (from system down to integrated circuits). Motivated by the wide appeal of Approximate Computing over the last 10 years, we conduct a two-part survey to cover key aspects (e.g., terminology and applications) and review the state-of-the art approximation techniques from all layers of the traditional computing stack. Part II of the survey classifies and presents the technical details of application-specific and architectural approximation techniques, which both target the design of resource-efficient processors/accelerators and systems. Moreover, it reports a quantitative analysis of the techniques and a detailed analysis of the application spectrum of Approximate Computing, and finally, it discusses open challenges and future directions.

2023-07-20T15:54:33Z Published in ACM Computing Surveys (Volume 57, Issue 7, 2025) ACM Computing Surveys, Volume 57, Issue 7, Article 177, 2025 Vasileios Leon Muhammad Abdullah Hanif Giorgos Armeniakos Xun Jiao Muhammad Shafique Kiamal Pekmestzi Dimitrios Soudris 10.1145/3711683 http://arxiv.org/abs/2307.11124v2 2025-03-19T19:53:53Z

The rapid growth of demanding applications in domains applying multimedia processing and machine learning has marked a new era for edge and cloud computing. These applications involve massive data and compute-intensive tasks, and thus, typical computing paradigms in embedded systems and data centers are stressed to meet the worldwide demand for high performance. Concurrently, over the last 15 years, the semiconductor industry has established power efficiency as a first-class design concern. As a result, the community of computing systems is forced to find alternative design approaches to facilitate high-performance and power-efficient computing. Among the examined solutions, Approximate Computing has attracted an ever-increasing interest, which has resulted in novel approximation techniques for all the layers of the traditional computing stack. More specifically, during the last decade, a plethora of approximation techniques in software (programs, frameworks, compilers, runtimes, languages), hardware (circuits, accelerators), and architectures (processors, memories) have been proposed in the literature. The current article is Part I of a comprehensive survey on Approximate Computing. It reviews its motivation, terminology and principles, as well it classifies the state-of-the-art software & hardware approximation techniques, presents their technical details, and reports a comparative quantitative analysis.

2023-07-20T15:41:06Z Published in ACM Computing Surveys (Volume 57, Issue 7, 2025) ACM Computing Surveys, Volume 57, Issue 7, Article 185, 2025 Vasileios Leon Muhammad Abdullah Hanif Giorgos Armeniakos Xun Jiao Muhammad Shafique Kiamal Pekmestzi Dimitrios Soudris 10.1145/3716845 http://arxiv.org/abs/2306.00642v4 2025-03-19T16:36:33Z

We introduce the framework FreeCHR which formalizes the embedding of Constraint Handling Rules (CHR) into a host language, using the concept of initial algebra semantics from category theory. We hereby establish a high-level implementation scheme for CHR as well as a common formalization for both theory and practice. We propose a lifting of the syntax of CHR via an endofunctor in the category Set and a lifting of the very abstract operational semantics of CHR into FreeCHR, using the free algebra, generated by the endofunctor. We give proofs for soundness and completeness w.r.t. its original definition. We also propose a first abstract execution algorithm and prove correctness w.r.t. the operational semantics. Finally, we show the practicability of our approach by giving two possible implementations of this algorithm in Haskell and Python. Under consideration in Theory and Practice of Logic Programming (TPLP).

2023-06-01T13:08:50Z Extended version of the original paper which was presented at the 7th International Joint Conference on Rules and Reasoning (RuleML+RR 2023). Under consideration in Theory and Practice of Logic Programming (TPLP) Sascha Rechenberger Thom Frühwirth 10.1017/S1471068425000043 http://arxiv.org/abs/2411.07718v4 2025-03-19T14:54:07Z

Structured code differencing is the act of comparing the hierarchical structure of code via its abstract syntax tree (AST) to capture modifications. AST-based source code differencing enables tasks such as vulnerability detection and automated repair where traditional line-based differencing falls short. We introduce SoliDiffy, the first AST differencing tool for Solidity smart contracts with the ability to generate an edit script that soundly shows the structural differences between two smart-contracts using insert, delete, update, move operations. In our evaluation on 353,262 contract pairs, SoliDiffy achieved a 96.1% diffing success rate, surpassing the state-of-the-art, and produced significantly shorter edit scripts. Additional experiments on 925 real-world commits further confirmed its superiority compared to Git line-based differencing. SoliDiffy provides accurate representations of smart contract evolution even in the existence of multiple complex modifications to the source code. SoliDiffy is made publicly available at https://github.com/mojtaba-eshghie/SoliDiffy.

2024-11-12T11:19:54Z Mojtaba Eshghie Viktor Åryd Cyrille Artho Martin Monperrus http://arxiv.org/abs/2410.15081v4 2025-03-19T11:03:59Z

Probabilistic programming is becoming increasingly popular thanks to its ability to specify problems with a certain degree of uncertainty. In this work, we focus on term rewriting, a well-known computational formalism. In particular, we consider systems that combine traditional rewriting rules with probabilities. Then, we define a novel "distribution semantics" for such systems that can be used to model the probability of reducing a term to some value. We also show how to compute a set of "explanations" for a given reduction, which can be used to compute its probability in a more efficient way. Finally, we illustrate our approach with several examples and outline a couple of extensions that may prove useful to improve the expressive power of probabilistic rewrite systems.

2024-10-19T12:00:13Z Submitted for publication Germán Vidal http://arxiv.org/abs/2503.15571v1 2025-03-19T11:01:00Z

Data profiling is critical in machine learning for generating descriptive statistics, supporting both deeper understanding and downstream tasks like data valuation and curation. This work addresses profiling specifically in the context of code datasets for Large Language Models (code-LLMs), where data quality directly influences tasks such as code generation and summarization. Characterizing code datasets in terms of programming language concepts enables better insights and targeted data curation. Our proposed methodology decomposes code data profiling into two phases: (1) an offline phase where LLMs are leveraged to derive and learn rules for extracting syntactic and semantic concepts across various programming languages, including previously unseen or low-resource languages, and (2) an online deterministic phase applying these derived rules for efficient real-time analysis. This hybrid approach is customizable, extensible to new syntactic and semantic constructs, and scalable to multiple languages. Experimentally, our LLM-aided method achieves a mean accuracy of 90.33% for syntactic extraction rules and semantic classification accuracies averaging 80% and 77% across languages and semantic concepts, respectively.

2025-03-19T11:01:00Z 21 pages Pankaj Thorat Adnan Qidwai Adrija Dhar Aishwariya Chakraborty Anand Eswaran Hima Patel Praveen Jayachandran http://arxiv.org/abs/2410.15908v2 2025-03-19T10:19:30Z

We report our experience formally modelling and verifying CXL.cache, the inter-device cache coherence protocol of the Compute Express Link standard. We have used the Isabelle proof assistant to create a formal model for CXL.cache based on the prose English specification. This led to us identifying and proposing fixes to several problems we identified as unclear, ambiguous or inaccurate, some of which could lead to incoherence if left unfixed. Nearly all our issues and proposed fixes have been confirmed and tentatively accepted by the CXL consortium for adoption, save for one which is still under discussion. To validate the faithfulness of our model we performed scenario verification of essential restrictions such as "Snoop-pushes-GO", and produced a fully mechanised proof of a coherence property of the model. The considerable size of this proof, comprising tens of thousands of lemmas, prompted us to develop new proof automation tools, which we have made available for other Isabelle users working with similarly cumbersome proofs.

2024-10-21T11:29:49Z 14 pages Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS 2025, Rotterdam, Netherlands Chengsong Tan Alastair F. Donaldson John Wickerson 10.1145/3676641.3715999 http://arxiv.org/abs/2407.11816v3 2025-03-18T23:42:19Z

Effect handlers are a powerful abstraction for defining, customising, and composing computational effects. Statically ensuring that all effect operations are handled requires some form of effect system, but using a traditional effect system would require adding extensive effect annotations to the millions of lines of existing code in these languages. Recent proposals seek to address this problem by removing the need for explicit effect polymorphism. However, they typically rely on fragile syntactic mechanisms or on introducing a separate notion of second-class function. We introduce a novel approach based on modal effect types.

2024-07-16T15:07:01Z Wenhao Tang Leo White Stephen Dolan Daniel Hillerström Sam Lindley Anton Lorenzen http://arxiv.org/abs/2503.14183v1 2025-03-18T11:58:00Z

Although formal methods are capable of producing reliable software, they have seen minimal adoption in everyday programming. Automatic code generation using large language models is becoming increasingly widespread, but it rarely considers producing strong correctness guarantees. In this study, we explore the ability of LLMs to produce verified code in three verification languages (Dafny, Nagini, and Verus). To do so, we use manually curated datasets derived from the state-ofthe-art Python benchmark, HumanEval. We also assess what types of information are sufficient to achieve good-quality results.

2025-03-18T11:58:00Z Aleksandr Shefer Igor Engel Stanislav Alekseev Daniil Berezun Ekaterina Verbitskaia Anton Podkopaev http://arxiv.org/abs/2303.05244v6 2025-03-18T09:15:50Z

Multiple types can represent the same concept. For example, lists and trees can both represent sets. Unfortunately, this easily leads to incomplete libraries: some set-operations may only be available on lists, others only on trees. Similarly, subtypes and quotients are commonly used to construct new type abstractions in formal verification. In such cases, one often wishes to reuse operations on the representation type for the new type abstraction, but to no avail: the types are not the same. To address these problems, we present a new framework that transports programs via equivalences. Existing transport frameworks are either designed for dependently typed, constructive proof assistants, use univalence, or are restricted to partial quotient types. Our framework (1) is designed for simple type theory, (2) generalises previous approaches working on partial quotient types, and (3) is based on standard mathematical concepts, particularly Galois connections and equivalences. We introduce the notion of partial Galois connections and equivalences and prove their closure properties under (dependent) function relators, (co)datatypes, and compositions. We formalised the framework in Isabelle/HOL and provide a prototype. This is the extended version of "Transport via Partial Galois Connections and Equivalences", 21st Asian Symposium on Programming Languages and Systems, 2023.

2023-03-09T13:30:55Z 18 pages; extended version from 21st Asian Symposium on Programming Languages and Systems, 2023 Asian Symposium on Programming Languages and Systems APLAS 2023: Programming Languages and Systems, 225-245 Kevin Kappelmann 10.1007/978-981-99-8311-7_11 http://arxiv.org/abs/2503.13970v1 2025-03-18T07:08:39Z

In recent years, there has been extensive research on how to extend general-purpose programming language semantics with domain-specific modeling constructs. Two areas of particular interest are (i) universal probabilistic programming where Bayesian probabilistic models are encoded as programs, and (ii) differentiable programming where differentiation operators are first class or differential equations are part of the language semantics. These kinds of languages and their language constructs are usually studied separately or composed in restrictive ways. In this paper, we study and formalize the combination of probabilistic programming constructs, first-class differentiation, and ordinary differential equations in a higher-order setting. We propose formal semantics for a core of such differentiable probabilistic programming language (DPPL), where the type system tracks random computations and rejects unsafe compositions during type checking. The semantics and its type system are formalized, mechanized, and proven sound in Agda with respect to abstract language constructs.

2025-03-18T07:08:39Z Oscar Eriksson Anders Ågren Thuné Johannes Borgström David Broman http://arxiv.org/abs/2503.13084v1 2025-03-17T11:44:37Z

Quantum computing leverages the principles of quantum mechanics to perform computations far beyond the capabilities of classical systems, particularly in fields such as cryptography and optimization. However, current quantum programming languages often require low-level implementation, posing significant barriers for many developers due to their steep learning curve and limited abstraction. In response, we introduce \textbf{Qutes}, a high-level quantum programming language designed to simplify quantum algorithm development while maintaining the flexibility required for advanced applications. By abstracting complex quantum operations and allowing intuitive expressions through high-level constructs, Qutes enables users to write efficient quantum programs without extensive knowledge of quantum mechanics or circuit design. Built upon Qiskit, Qutes translates its syntax directly into executable quantum code, facilitating seamless integration with quantum hardware. This paper provides an overview of the language's architecture, core functionalities, and its ability to unify classical and quantum operations within a single framework. Additionally, we demonstrate Qutes' application in key quantum algorithms, showcasing its potential to make quantum programming more accessible and practical for a wider range of developers and researchers.

2025-03-17T11:44:37Z Simone Faro Francesco Pio Marino Gabriele Messina http://arxiv.org/abs/1712.05465v4 2025-03-17T09:19:39Z

Choreographic programming promises a simple approach to the coding of concurrent and distributed systems: write the collective communication behaviour of a system of processes as a choreography, and then the programs for these processes are automatically compiled by a provably-correct procedure known as endpoint projection. While this promise prompted substantial research, a theory that can deal with realistic communication failures in a distributed network remains elusive. In this work, we provide the first theory of choreographic programming that addresses realistic communication failures taken from the literature of distributed systems: processes can send or receive fewer messages than they should (send and receive omission), and the network can fail at transporting messages (omission failure). Our theory supports the programming of strategies for failure recovery, and a novel static analysis (called robustness) to check for delivery guarantees (at-most-once and exactly-once). Our key technical innovation is a deconstruction of the usual communication primitive in choreographies to allow for independent implementations of the send and receive actions of a communication, while still retaining the static guarantee that these actions will correlate correctly (the essence of choreographic programming). This has two main benefits. First, each side of a communication can adopt its own failure recovery strategy, as in realistic protocols. Second, initiating new communications does not require any (unrealistic) synchronisation over unreliable channels: senders and receivers agree by construction on how each message should be identified. We validate our design via a series of examples -- including two-phase commit, which so far eluded choreographic programming -- and an implementation of our ideas in the choreographic programming language Choral.

2017-12-14T21:56:41Z IMADA-preprint Eva Graversen Fabrizio Montesi Marco Peressotti http://arxiv.org/abs/2501.18874v2 2025-03-14T17:33:20Z

A compromised system component can issue message sequences that are legal while also leading the overall system into unsafe states. Such stealthy attacks are challenging to characterize, because message interfaces in standard languages specify each individual message separately but do not specify safe sequences of messages. We present initial results from ongoing work applying refined multiparty session types as a mechanism for expressing and enforcing proper message usage to exclude unsafe sequences. We illustrate our approach by using refined multiparty session types to mitigate safety and security issues in the MAVLink protocol commonly used in UAVs.

2025-01-31T03:56:35Z To be featured in proceedings of The 17th NASA Formal Methods Symposium Arthur Amorim Max Taylor Trevor Kann William L. Harrison Gary T. Leavens Lance Joneckis http://arxiv.org/abs/2404.04662v4 2025-03-14T14:34:56Z

Formal verification is only as good as the specification of a system, which is also true for neural network verification. Existing specifications follow the paradigm of data as specification, where the local neighborhood around a reference data point is considered correct or robust. While these specifications provide a fair testbed for assessing model robustness, they are too restrictive for verifying any unseen test data points, a challenging task with significant real-world implications. Recent work shows great promise through a new paradigm, neural representation as specification, which uses neural activation patterns (NAPs) for this purpose. However, it computes the most refined NAPs, which include many redundant neurons. In this paper, we study the following problem: Given a neural network, find a minimal (general) NAP specification that is sufficient for formal verification of its robustness properties. Finding the minimal NAP specification not only expands verifiable bounds but also provides insights into which set of neurons contributes to the model's robustness. To address this problem, we propose three approaches: conservative, statistical, and optimistic. Each of these methods offers distinct strengths and trade-offs in terms of minimality and computational speed, making them suitable for scenarios with different priorities. Notably, the optimistic approach can probe potential causal links between neurons and the robustness of large vision neural networks without relying on verification tools, a task existing methods struggle to scale. Our experiments show that minimal NAP specifications use far fewer neurons than those from previous work while expanding verifiable boundaries by several orders of magnitude.

2024-04-06T15:31:20Z 30 pages,7 figures Chuqin Geng Zhaoyue Wang Haolin Ye Xujie Si