https://arxiv.org/api/Qb27ZBa1n/Lo9oejQ2aap0lfs/U 2026-06-30T17:34:38Z 9958 1965 15 http://arxiv.org/abs/2412.10632v1 2024-12-14T01:18:32Z

We propose a method for conducting algebraic program analysis (APA) incrementally in response to changes of the program under analysis. APA is a program analysis paradigm that consists of two distinct steps: computing a path expression that succinctly summarizes the set of program paths of interest, and interpreting the path expression using a properly-defined semantic algebra to obtain program properties of interest. In this context, the goal of an incremental algorithm is to reduce the analysis time by leveraging the intermediate results computed before the program changes. We have made two main contributions. First, we propose a data structure for efficiently representing path expression as a tree together with a tree-based interpreting method. Second, we propose techniques for efficiently updating the program properties in response to changes of the path expression. We have implemented our method and evaluated it on thirteen Java applications from the DaCapo benchmark suite. The experimental results show that both our method for incrementally computing path expression and our method for incrementally interpreting path expression are effective in speeding up the analysis. Compared to the baseline APA and two state-of-the-art APA methods, the speedup of our method ranges from 160X to 4761X depending on the types of program analyses performed.

2024-12-14T01:18:32Z Chenyu Zhou Yuzhou Fang Jingbo Wang Chao Wang http://arxiv.org/abs/2402.18708v2 2024-12-12T23:33:14Z

We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.

2024-02-28T21:14:21Z 23 pages + 53 pages of appendix Proc. ACM Program. Lang. 9, POPL, Article 58 (January 2025) Jialu Bao Emanuele D'Osualdo Azadeh Farzan 10.1145/3704894 http://arxiv.org/abs/2412.16185v1 2024-12-12T14:01:55Z

The FRACTRAN programs $\sqrt{2}$GAME and NR$\sqrt{2}$GAME are presented, both of which compute the decimal expansion of $\sqrt{2}$. Our $\sqrt{2}$GAME is analogous to Conway's PIGAME program. In fact, our proof carries over to PIGAME to produce a simpler proof of Conway's theorem as well as highlight how the efficiency of the program can be improved. NR$\sqrt{2}$GAME encodes the canonical example of the Newton--Raphson method in FRACTRAN.

2024-12-12T14:01:55Z Khushi Kaushik Tommy Murphy David Weed http://arxiv.org/abs/2411.09347v2 2024-12-12T10:54:13Z

Static single assignment form, or SSA, has been the dominant compiler intermediate representation for decades. In this paper, we give a type theory for a variant of SSA, including its equational theory, which are strong enough to validate a variety of control and data flow transformations. We also give a categorical semantics for SSA, and show that the type theory is sound and complete with respect to the categorical axiomatization. We demonstrate the utility of our model by exhibiting a variety of concrete models satisfying our axioms, including in particular a model of TSO weak memory. The correctness of the syntactic metatheory, as well as the completeness proof has been mechanized in the Lean proof assistant.

2024-11-14T10:48:28Z 95 pages, 38 figures, mechanization available at https://github.com/imbrem/debruijn-ssa/tree/toplas-artifact Jad Elkhaleq Ghalayini Neel Krishnaswami http://arxiv.org/abs/2412.08739v1 2024-12-11T19:17:28Z

Over the past two decades, the Web Ontology Language (OWL) has been instrumental in advancing the development of ontologies and knowledge graphs, providing a structured framework that enhances the semantic integration of data. However, the reliability of deductive reasoning within these systems remains challenging, as evidenced by inconsistencies among popular reasoners in recent competitions. This evidence underscores the limitations of current testing-based methodologies, particularly in high-stakes domains such as healthcare. To mitigate these issues, in this paper, we have developed VEL, a formally verified EL++ reasoner equipped with machine-checkable correctness proofs that ensure the validity of outputs across all possible inputs. This formalization, based on the algorithm of Baader et al., has been transformed into executable OCaml code using the Coq proof assistant's extraction capabilities. Our formalization revealed several errors in the original completeness proofs, which led to changes to the algorithm to ensure its completeness. Our work demonstrates the necessity of mechanization of reasoning algorithms to ensure their correctness at theoretical and implementation levels.

2024-12-11T19:17:28Z Atalay Mert Ileri Nalen Rangarajan Jack Cannell Hande McGinty http://arxiv.org/abs/2412.12163v1 2024-12-11T18:44:31Z

Large Language Models (LLMs) have demonstrated great potential in various language processing tasks, and recent studies have explored their application in compiler optimizations. However, all these studies focus on the conventional open-source LLMs, such as Llama2, which lack enhanced reasoning mechanisms. In this study, we investigate the errors produced by the fine-tuned 7B-parameter Llama2 model as it attempts to learn and apply a simple peephole optimization for the AArch64 assembly code. We provide an analysis of the errors produced by the LLM and compare it with state-of-the-art OpenAI models which implement advanced reasoning logic, including GPT-4o and GPT-o1 (preview). We demonstrate that OpenAI GPT-o1, despite not being fine-tuned, outperforms the fine-tuned Llama2 and GPT-4o. Our findings indicate that this advantage is largely due to the chain-of-thought reasoning implemented in GPT-o1. We hope our work will inspire further research on using LLMs with enhanced reasoning mechanisms and chain-of-thought for code generation and optimization.

2024-12-11T18:44:31Z 13 pages, 8 figures Xiangxin Fang Lev Mukhanov http://arxiv.org/abs/2404.18353v2 2024-12-11T13:02:30Z

This study compares state-of-the-art Large Language Models (LLMs) on their tendency to generate vulnerabilities when writing C programs using a neutral zero-shot prompt. Tihanyi et al. introduced the FormAI dataset at PROMISE'23, featuring 112,000 C programs generated by GPT-3.5-turbo, with over 51.24% identified as vulnerable. We extended that research with a large-scale study involving 9 state-of-the-art models such as OpenAI's GPT-4o-mini, Google's Gemini Pro 1.0, TII's 180 billion-parameter Falcon, Meta's 13 billion-parameter Code Llama, and several other compact models. Additionally, we introduce the FormAI-v2 dataset, which comprises 331 000 compilable C programs generated by these LLMs. Each program in the dataset is labeled based on the vulnerabilities detected in its source code through formal verification, using the Efficient SMT-based Context-Bounded Model Checker (ESBMC). This technique minimizes false positives by providing a counterexample for the specific vulnerability and reduces false negatives by thoroughly completing the verification process. Our study reveals that at least 62.07% of the generated programs are vulnerable. The differences between the models are minor, as they all show similar coding errors with slight variations. Our research highlights that while LLMs offer promising capabilities for code generation, deploying their output in a production environment requires proper risk assessment and validation.

2024-04-29T01:24:14Z Accepted and will be shortly published at Empirical Software Engineering (EMSE). Journal Impact Factor: 3.5 (2023) Norbert Tihanyi Tamas Bisztray Mohamed Amine Ferrag Ridhi Jain Lucas C. Cordeiro 10.1007/s10664-024-10590-1. http://arxiv.org/abs/2412.08235v1 2024-12-11T09:32:11Z

Process algebras have been widely used to verify security protocols in a formal manner. However they mostly focus on synchronous communication based on the exchange of messages. We present an alternative approach relying on asynchronous communication obtained through information available on a shared space. More precisely this paper first proposes an embedding in Scala of a Linda-like language, called Bach. It consists of a Domain Specific Language, internal to Scala, that allows us to experiment programs developed in Bach while benefiting from the Scala eco-system, in particular from its type system as well as program fragments developed in Scala. Moreover, we introduce a logic that allows to restrict the executions of programs to those meeting logic formulae. Our work is illustrated on the Needham-Schroeder security protocol, for which we manage to automatically rediscover the man-in-the-middle attack first put in evidence by G. Lowe.

2024-12-11T09:32:11Z In Proceedings ICE 2024, arXiv:2412.07570 EPTCS 414, 2024, pp. 58-76 Doha Ouardi University of Namur Manel Barkallah University of Namur Jean-Marie Jacquet University of Namur 10.4204/EPTCS.414.4 http://arxiv.org/abs/2412.08233v1 2024-12-11T09:31:40Z

We propose an overview of the decentralized reconfiguration language Concerto-D through its Maude formalization. Concerto-D extends the already published Concerto language. Concerto-D improves on two different parameters compared with related work: the decentralized coordination of numerous local reconfiguration plans which avoid a single point of failure when considering unstable networks such as edge computing, or cyber-physical systems (CPS) for instance; and a mechanized formal semantics of the language with Maude which offers guarantees on the executability of the semantics. Throughout the paper, the Concerto-D language and its semantics are exemplified with a reconfiguration extracted from a real case study on a CPS. We rely on the Maude formal specification language, which is based on rewriting logic, and consequently perfectly suited for describing a concurrent model.

2024-12-11T09:31:40Z In Proceedings ICE 2024, arXiv:2412.07570 EPTCS 414, 2024, pp. 21-38 Farid Arfi IMT Atlantique Hélène Coullon IMT Atlantique Frédéric Loulergue University of Orleans Jolan Philippe IMT Atlantique Simon Robillard University of Montpellier 10.4204/EPTCS.414.2 http://arxiv.org/abs/2412.08232v1 2024-12-11T09:31:24Z

While formal models of concurrency tend to focus on synchronous communication, asynchronous communication is relevant in practice. In this paper, we will discuss asynchronous communication in the context of session-based concurrency, the model of computation in which session types specify the structure of the two-party protocols implemented by the channels of a communicating process. We overview recent work on addressing the challenge of ensuring the deadlock-freedom property for message-passing processes that communicate asynchronously in cyclic process networks governed by session types. We offer a gradual presentation of three typed process frameworks and outline how they may be used to guarantee deadlock freedom for a concurrent functional language with sessions.

2024-12-11T09:31:24Z In Proceedings ICE 2024, arXiv:2412.07570 EPTCS 414, 2024, pp. 1-20 Bas van den Heuvel Karlsruhe University of Applied Sciences, Karlsruhe, and University of Freiburg, Freiburg, Germany Jorge A. Pérez University of Groningen, The Netherlands 10.4204/EPTCS.414.1 http://arxiv.org/abs/2412.08035v1 2024-12-11T02:31:46Z

Large language models (LLMs) show promise in code translation due to their ability to generate idiomatic code. However, a significant limitation when using LLMs for code translation is scalability: existing works have shown a drop in translation success rates for code exceeding around 100 lines. We overcome this limitation by developing a modular approach to translation, where we partition the code into small code fragments which can be translated independently and semantically validated (that is, checking I/O equivalence). When this approach is applied naively, we discover that LLMs are unreliable when translating features of the source language that do not have a direct mapping to the target language, and that the LLM often gets stuck in repair loops when attempting to fix errors. To address these issues, we introduce two key concepts: (1) feature mapping, which integrates predefined translation rules with LLM-based translation to guide the LLM in navigating subtle language differences and producing semantically accurate code; and (2) type-compatibility, which facilitates localized checks at the function signature level to detect errors early, thereby narrowing the scope of potential repairs. We apply our approach to translating real-world Go codebases to Rust, demonstrating that we can consistently generate reliable Rust translations for projects up to 6,600 lines of code and 369 functions, with an average of 73% of functions successfully validated for I/O equivalence, considerably higher than any existing work.

2024-12-11T02:31:46Z Hanliang Zhang Cristina David Meng Wang Brandon Paulsen Daniel Kroening http://arxiv.org/abs/2211.09572v3 2024-12-10T10:21:04Z

Static analysis by abstract interpretation is generally designed to be "sound", that is, it should not claim to establish properties that do not hold-in other words, not provide "false negatives" about possible bugs. A rarer requirement is that it should be "complete", meaning that it should be able to infer certain properties if they hold. This paper describes a number of practical issues and questions related to completeness that I have come across over the years.

2022-11-17T14:55:31Z Vincenzo Arceri; Agostino Cortesi; Pietro Ferrara; Martina Olliaro. Challenges of Software Verification, 238, Springer Nature Singapore, pp.93-108, 2023, Intelligent Systems Reference Library, 978-981-19-9600-9 David Monniaux VERIMAG - IMAG 10.1007/978-981-19-9601-6_6 http://arxiv.org/abs/2412.07235v1 2024-12-10T06:54:42Z

We propose a verified executable Scala backend for ASN1SCC, a compiler for ASN.1/ACN. ASN.1 is a language for describing data structures widely employed in ground and space telecommunications. ACN can be used along ASN.1 to describe complex binary formats and legacy protocols. To avoid error-prone and time-consuming manual writing of serializers, we show how to port an ASN.1/ACN code generator to generate Scala code. We then enhance the generator to emit not only the executable code but also strong enough pre-conditions, post-conditions, and lemmas for inductive proofs. This allowed us to verify the resulting generated annotated code using Stainless, a program verifier for Scala. The properties we prove include the absence of runtime errors, such as out-of-bound accesses or divisions by zero. For the base library, we also prove the invertibility of the decoding and encoding functions, showing that decoding yields the encoded value back. Furthermore, our system automatically inserts invertibility proofs for arbitrary records in the generated code, proving over 300'000 verification conditions. We establish key steps towards such proofs for sums and arrays as well.

2024-12-10T06:54:42Z Mario Bucev Samuel Chassot Simon Felix Filip Schramka Viktor Kunčak http://arxiv.org/abs/2412.16179v1 2024-12-10T02:42:31Z

The ubiquity of networking infrastructure in modern life necessitates scrutiny into networking fundamentals to ensure the safety and security of that infrastructure. The formalization of concurrent algorithms, a cornerstone of networking, is a longstanding area of research in which models and frameworks describing distributed systems are established. Despite its long history of study, the challenge of concisely representing and verifying concurrent algorithms remains unresolved. Existing formalisms, while powerful, often fail to capture the dynamic nature of real-world concurrency in a manner that is both comprehensive and scalable. This paper explores the evolution of formal models of concurrency over time, investigating their generality and utility for reasoning about real-world networking programs. Four foundational papers on formal concurrency are considered: Hoare's Parallel programming: An axiomatic approach, Milner's A Calculus of Mobile Processes, O'Hearn's Resources, Concurrency and Local Reasoning, and the recent development of Coq's Iris framework.

2024-12-10T02:42:31Z 10 pages, 2 figures Charles Averill http://arxiv.org/abs/2412.07086v1 2024-12-10T01:03:36Z

When proving the correctness of a method for slicing probabilistic programs, it was previously discovered by the authors that for a fixed point iteration to work one needs a non-standard starting point for the iteration. This paper presents and explores this technique in a general setting; it states the lemmas that must be established to use the technique to prove the correctness of a program transformation, and sketches how to apply the technique to slicing of probabilistic programs.

2024-12-10T01:03:36Z To be published by Springer in Festschrift for Alan Mycroft Torben Amtoft Anindya Banerjee