https://arxiv.org/api/euTDXvLANce3F27tXouZv6QC6eY 2026-06-29T01:47:53Z 9954 1740 15 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 http://arxiv.org/abs/2503.07273v2 2025-03-14T13:33:00Z

We study a theory of asynchronous session types ensuring that well-typed processes terminate under a suitable fairness assumption. Fair termination entails starvation freedom and orphan message freedom namely that all messages, including those that are produced early taking advantage of asynchrony, are eventually consumed. The theory is based on a novel fair asynchronous subtyping relation for session types that is coarser than the existing ones. The type system is also the first of its kind that is firmly rooted in linear logic: fair asynchronous subtyping is incorporated as a natural generalization of the cut and axiom rules of linear logic and asynchronous communication is modeled through a suitable set of commuting conversions and of deep cut reductions in linear logic proofs.

2025-03-10T12:53:57Z Luca Padovani Gianluigi Zavattaro http://arxiv.org/abs/2503.11288v1 2025-03-14T10:52:48Z

JSON Schema is a logical language used to define the structure of JSON values. JSON Schema syntax is based on nested schema objects. In all versions of JSON Schema until Draft-07, collectively known as Classical JSON Schema, the semantics of a schema was entirely described by the set of JSON values that it validates. This semantics was the basis for a thorough theoretical study and for the development of tools to decide satisfiability and equivalence of schemas. Unfortunately, Classical JSON Schema suffered a severe limitation in its ability to express extensions of object schemas, which caused the introduction, with Draft 2019-09, of two disruptive features: annotation dependency and dynamic references. These new features undermine the previously developed semantic theory, and the algorithms used to decide satisfiability for Classical JSON Schema are not easy to extend. One possible solution is rewriting a schema written in Modern JSON Schema into an equivalent schema in Classical JSON Schema. In this paper we prove that the elimination of annotation dependent keywords cannot, in general, avoid an exponential increase of the schema dimension. We provide an algorithm to eliminate these keywords that, despite the theoretical lower bound, behaves quite well in practice, as we verify with an extensive set of experiments.

2025-03-14T10:52:48Z Lyes Attouche Mohamed-Amine Baazizi Dario Colazzo Giorgio Ghelli Stefan Klessinger Carlo Sartiani Stefanie Scherzinger http://arxiv.org/abs/2503.10855v1 2025-03-13T20:09:09Z

Modern computing systems increasingly rely on composing heterogeneous devices to improve performance and efficiency. Programming these systems is often unproductive: algorithm implementations must be coupled to system-specific logic, including device-specific optimizations, partitioning, and inter-device communication and synchronization, which requires developing different programs for different system configurations. We propose the Juno language, which represents general purpose applications in an imperative form that can be transformed into parallel, optimized, system-specific code using an expressive and granular imperative scheduling language. We also introduce the Hercules compiler, which uses a novel intermediate representation to represent general and device-specific parallel code in a manner that is easy to analyze and manipulate using schedules. Our system achieves competitive performance with hand-optimized device-specific code (geomean speedups of $1.25\times$ and $1.48\times$ on the CPU and GPU) and significantly outperforms a prior general purpose heterogeneous programming system (geomean speedups of $9.31\times$ and $16.18\times$ on the CPU and GPU).

2025-03-13T20:09:09Z Russel Arbore Aaron Councilman Xavier Routh Ryan Ziegler Praneet Rathi Vikram Adve http://arxiv.org/abs/2503.10416v1 2025-03-13T14:36:48Z

Runtime repeated recursion unfolding was recently introduced as a just-in-time program transformation strategy that can achieve super-linear speedup. So far, the method was restricted to single linear direct recursive rules in the programming language Constraint Handling Rules (CHR). In this companion paper, we generalize the technique to multiple recursion and to multiple recursive rules and provide an implementation of the generalized method in the logic programming language Prolog. The basic idea of the approach is as follows: When a recursive call is encountered at runtime, the recursive rule is unfolded with itself and this process is repeated with each resulting unfolded rule as long as it is applicable to the current call. In this way, more and more recursive steps are combined into one recursive step. Then an interpreter applies these rules to the call starting from the most unfolded rule. For recursions which have sufficiently simplifyable unfoldings, a super-linear can be achieved, i.e. the time complexity is reduced. We implement an unfolder, a generalized meta-interpreter and a novel round-robin rule processor for our generalization of runtime repeated recursion unfolding with just ten clauses in Prolog. We illustrate the feasibility of our technique with worst-case time complexity estimates and benchmarks for some basic classical algorithms that achieve a super-linear speedup.

2025-03-13T14:36:48Z arXiv admin note: substantial text overlap with arXiv:2307.02180 Thom Fruehwirth http://arxiv.org/abs/2308.02018v4 2025-03-12T20:25:10Z

Reasoning about the sensitivity of functions with respect to their inputs has interesting applications in various areas, such as differential privacy. In order to check and enforce sensitivity, several approaches have been developed, notably sensitivity type systems. In these systems, sensitivity can be seen as an effect in the sense of type-and-effects systems as originally proposed by Gifford and Lucassen. Because type-and-effect systems can make certain useful programming patterns tedious or overly conservative, there is value in bringing the benefits of gradual typing to these disciplines in order to ease their adoption. In this work, we motivate, formalize, and prototype gradual sensitivity typing. The language GSoul supports both the unrestricted unknown sensitivity and bounded imprecision in the form of intervals. Gradual sensitivity typing allows programmers to smoothly evolve typed programs without any static sensitivity information towards hardened programs with a mix of static and dynamic sensitivity checking. In particular, we show that gradual sensitivity supports recursive functions for which fully static checking would be overly conservative, seamlessly enabling exact runtime sensitivity checks. GSoul satisfies both the gradual guarantees and sensitivity type soundness, known as metric preservation. We establish that, in general, gradual metric preservation is termination insensitive, and that one can achieve termination-sensitive gradual metric preservation by hardening specifications to bounded imprecision. We implement a prototype that provides an interactive test bed for gradual sensitivity typing. This work opens the door to gradualizing other typing disciplines that rely on function sensitivity such as differential privacy, as well as other quantitative type-based reasoning techniques.

2023-08-03T20:19:49Z Camera ready, to appear at CSF'25 Damian Arquez Matías Toro Éric Tanter http://arxiv.org/abs/2404.08106v2 2025-03-12T17:12:53Z

Many interesting program properties involve the execution of multiple programs, including observational equivalence, noninterference, co-termination, monotonicity, and idempotency. One strategy for verifying such relational properties is to construct and reason about an intermediate program whose correctness implies that the individual programs exhibit those properties. A key challenge in building an intermediate program is finding a good alignment of the original programs. An alignment puts subparts of the original programs into correspondence so that their similarities can be exploited in order to simplify verification. We propose an approach to intermediate program construction that uses e-graphs, equality saturation, and algebraic realignment rules to efficiently represent and build programs amenable to automated verification. A key ingredient of our solution is a novel data-driven extraction technique that uses execution traces of candidate intermediate programs to identify solutions that are semantically well-aligned. We have implemented a relational verification engine based on our proposed approach, called KestRel, and use it to evaluate our approach over a suite of benchmarks taken from the relational verification literature.

2024-04-11T20:06:43Z Robert Dickerson Prasita Mukherjee Benjamin Delaware http://arxiv.org/abs/2503.09463v1 2025-03-12T15:12:12Z

Co-developing scientific algorithms and hardware accelerators requires domain-specific knowledge and large engineering resources. This leads to a slow development pace and high project complexity, which creates a barrier to entry that is too high for the majority of developers to overcome. We are developing a reusable end-to-end compiler toolchain for the Julia language entirely built on permissively-licensed open-source projects. This unifies accelerator and algorithm development by automatically synthesising Julia source code into high-performance Verilog.

2025-03-12T15:12:12Z Accepted for presentation at the 5th Workshop on Languages, Tools, and Techniques for Accelerator Design (LATTE'25), March 30, 2025, Rotterdam, Netherlands Benedict Short Ian McInerney John Wickerson http://arxiv.org/abs/2503.15540v1 2025-03-12T00:36:43Z

Program synthesis from input-output examples, also called programming by example (PBE), has had tremendous impact on automating end-user tasks. Large language models (LLMs) have the ability to solve PBE tasks by generating code in different target languages, but they can fail unpredictably. To recover for failure, most approaches, such as self-reflection, use the LLM to solve the same task, but with a richer context. We introduce a novel technique that recovers from failure by constructing simpler subtasks for the LLM to solve. Our approach performs compositional program synthesis using LLMs, where LLM not only guides the decomposition of the PBE task into subtasks, but also solves the subtasks. We present different strategies for decomposing the original task. We experimentally show that our approach can solve challenging task instances that are not solved by self-reflection alone.

2025-03-12T00:36:43Z Ruhma Khan Sumit Gulwani Vu Le Arjun Radhakrishna Ashish Tiwari Gust Verbruggen http://arxiv.org/abs/2503.08928v1 2025-03-11T22:18:51Z

Gradually-typed languages feature a dynamic type that supports implicit coercions, greatly weakening the type system but making types easier to adopt. Understanding how developers use this dynamic type is a critical question for the design of useful and usable type systems. This paper reports on an in-progress corpus study of the dynamic type in Python, targeting 221 GitHub projects that use the mypy type checker. The study reveals eight patterns-of-use for the dynamic type, which have implications for future refinements of the mypy type system and for tool support to encourage precise type annotations.

2025-03-11T22:18:51Z Accepted to HATRA 2024 Dibri Nsofor Ben Greenman http://arxiv.org/abs/2503.08923v1 2025-03-11T22:13:26Z

Hardware verification is crucial in modern SoC design, consuming around 70% of development time. SystemVerilog assertions ensure correct functionality. However, existing industrial practices rely on manual efforts for assertion generation, which becomes increasingly untenable as hardware systems become complex. Recent research shows that Large Language Models (LLMs) can automate this process. However, proprietary SOTA models like GPT-4o often generate inaccurate assertions and require expensive licenses, while smaller open-source LLMs need fine-tuning to manage HDL code complexities. To address these issues, we introduce **VERT**, an open-source dataset designed to enhance SystemVerilog assertion generation using LLMs. VERT enables researchers in academia and industry to fine-tune open-source models, outperforming larger proprietary ones in both accuracy and efficiency while ensuring data privacy through local fine-tuning and eliminating costly licenses. The dataset is curated by systematically augmenting variables from open-source HDL repositories to generate synthetic code snippets paired with corresponding assertions. Experimental results demonstrate that fine-tuned models like Deepseek Coder 6.7B and Llama 3.1 8B outperform GPT-4o, achieving up to 96.88% improvement over base models and 24.14% over GPT-4o on platforms including OpenTitan, CVA6, OpenPiton and Pulpissimo. VERT is available at https://github.com/AnandMenon12/VERT.

2025-03-11T22:13:26Z 29 Pages Anand Menon Samit S Miftah Shamik Kundu Souvik Kundu Amisha Srivastava Arnab Raha Gabriel Theodor Sonnenschein Suvadeep Banerjee Deepak Mathaikutty Kanad Basu http://arxiv.org/abs/2405.16450v3 2025-03-11T12:52:28Z

Programmatic reinforcement learning (PRL) has been explored for representing policies through programs as a means to achieve interpretability and generalization. Despite promising outcomes, current state-of-the-art PRL methods are hindered by sample inefficiency, necessitating tens of millions of program-environment interactions. To tackle this challenge, we introduce a novel LLM-guided search framework (LLM-GS). Our key insight is to leverage the programming expertise and common sense reasoning of LLMs to enhance the efficiency of assumption-free, random-guessing search methods. We address the challenge of LLMs' inability to generate precise and grammatically correct programs in domain-specific languages (DSLs) by proposing a Pythonic-DSL strategy - an LLM is instructed to initially generate Python codes and then convert them into DSL programs. To further optimize the LLM-generated programs, we develop a search algorithm named Scheduled Hill Climbing, designed to efficiently explore the programmatic search space to improve the programs consistently. Experimental results in the Karel domain demonstrate our LLM-GS framework's superior effectiveness and efficiency. Extensive ablation studies further verify the critical role of our Pythonic-DSL strategy and Scheduled Hill Climbing algorithm. Moreover, we conduct experiments with two novel tasks, showing that LLM-GS enables users without programming skills and knowledge of the domain or DSL to describe the tasks in natural language to obtain performant programs.

2024-05-26T06:33:48Z Max Liu Chan-Hung Yu Wei-Hsu Lee Cheng-Wei Hung Yen-Chun Chen Shao-Hua Sun http://arxiv.org/abs/2205.00862v4 2025-03-10T20:04:02Z

Compilers are a prime target for formal verification, since compiler bugs invalidate higher-level correctness guarantees, but compiler changes may become more labor-intensive to implement, if they must come with proof patches. One appealing approach is to present compilers as sets of algebraic rewrite rules, which a generic engine can apply efficiently. Now each rewrite rule can be proved separately, with no need to revisit past proofs for other parts of the compiler. We present the first realization of this idea, in the form of a framework for the Coq proof assistant. Our new Coq command takes normal proved theorems and combines them automatically into fast compilers with proofs. We applied our framework to improve the Fiat Cryptography toolchain for generating cryptographic arithmetic, producing an extracted command-line compiler that is about 1000$\times$ faster while actually featuring simpler compiler-specific proofs.

2022-05-02T12:45:57Z 13th International Conference on Interactive Theorem Proving (ITP 2022) Jason Gross Andres Erbsen Jade Philipoom Rajashree Agrawal Adam Chlipala 10.4230/LIPIcs.ITP.2022.17