Machine learning for classification has seen numerous applications to complex, real-world tasks. Learned classifiers have become important artifacts of software systems that, like code, require careful analyses, maintenance, and evolution. Existing work on the formal verification of learned classifiers has mainly focused on the properties of individual classifiers, e.g., safety, fairness, or robustness, but not on analyzing the commonalities and differences of multiple classifiers. We present MLDiff, a novel approach to comparing learned classifiers based on querying agreements and disagreements between classifications, where one classifier is an alternative or variant of another. We present a prototypical implementation that leverages an encoding to SMT and can discover differences not (yet) seen in available datasets. Our prototype implements MLDiff for any combination of Decision Trees, Linear Support Vector Classification, Logistic Regression Classification, and Neural Networks. We evaluate it on classifiers trained on popular datasets in terms of performance and effectiveness of the analysis to discover disagreements between classifiers.
The design of complex cyber-physical systems increasingly relies on heterogeneous, multi-domain models, each capturing different system aspects. As these models evolve independently, inconsistencies may arise. Such inconsistencies remain difficult to detect due to gaps between the modelling domains. We propose to bridge this gap by introducing a formal notion of observables, inspired by physics, as measurable system properties, such that every model can constrain the possible values of an observable. We define a semantic framework where observables induce consistency relations and show that any such relation can be expressed using suitable observable semantics. To capture realistic engineering scenarios, we extend the framework with meta-model spanning and compound observable semantics, enabling the modular construction of complex constraints. We also provide encodings of these observable semantics back into the original framework, preserving the original results and showing that extensions remain expressively equivalent to initial ones. Finally, we discuss some practical implications of our framework, namely how observables can support cross-domain communication, separation of concerns, and extensibility, allowing consistency requirements to evolve as part of the modelling process.
Solidity, the most popular smart contract language, has two different kinds of data areas, called storage and memory. Storage is persistent across transactions and stored in the blockchain, while memory is volatile and does not survive a transaction. In storage, data structures are of value kind, with deep copy and no aliasing. In memory, data structures are of reference kind, with shallow copy and potential aliasing. We are concerned with deductive verification of smart contracts written in Solidity. Hence, we provide a logic formalisation of both data areas supporting efficient representation of the data areas, striking a balance between term size and on-demand case distinctions. We present a formalisation of the Solidity data types in both storage and memory, meeting the stated objectives. Specifically, we detail our representation of these data areas, discussing their differences and the challenges we encountered, such as value vs. reference semantics, object identity creation, and eager vs. lazy evaluation to delay proof effort until necessary.
Class invariants characterize valid object states throughout an object’s lifecycle and play an important role for software maintenance and evolution. Because invariants are rarely documented, software engineers resort to modern data-driven techniques for their inference. Recent automatic techniques require representative sets of invalid objects as negative training examples, which are hard to come by for programs with reference-based data structures such as search trees. For example, techniques adopting program mutation invalidate search tree objects well wrt. their payload, but they fail to introduce cycles, despite acyclicity being an important property of trees. In this paper, we analyze the limitations of program mutation for constructing invalid objects and propose state mutation as a complementary approach. Our approach first retrieves valid objects from program executions and then systematically mutates object references to obtain structurally invalid objects. An evaluation on a benchmark of diverse reference-based data structures shows that, unlike program mutation, state mutation effectively generates invalid objects with structural violations. Moreover, combining both approaches significantly outperforms either one and delivers diverse negative training examples that capture more facets of a given data structure, thereby permitting the inference of more precise class invariants.
Testing probabilistic programs is non-trivial due to their stochastic nature. Given an input, the program may produce different outcomes depending on the underlying stochastic choices in the program. This means testing the expected outcomes of probabilistic programs requires repeated test executions unlike deterministic programs where a single execution may suffice for each test input. This raises the following question: how many times should we run a probabilistic program to effectively test it? This work proposes a novel black-box unit testing method, ProbTest, for testing the outcomes of probabilistic programs. Our method is founded on the theory surrounding a well-known combinatorial problem, the coupon collector’s problem. Using this method, developers can write unit tests as usual without extra effort while the number of required test executions is determined automatically with statistical guarantees for the results. We implement ProbTest as a plug-in for PyTest, a well-known unit testing tool for python programs. Using this plug-in, developers can write unit tests similar to any other Python program and the necessary test executions are handled automatically. We evaluate the method on case studies from the Gymnasium reinforcement learning library and a randomized data structure.
Memory corruption is one of the oldest and most disruptive problems in computer security, through which attackers may maliciously alter the program control flow. Unsafe languages, such as C and C++, are prone to these types of vulnerability. A promising alternative is Rust, which ensures memory safety through proper compile-time checks with no penalties at run-time. However, the Rust compiler is not able to provide these guarantees when programmers use Rust unsafe features or integrate code written in an unsafe language through the Foreign Function Interface mechanism. If the unsafe features and the integration of unsafe code are not handled with extreme care, the memory errors that Rust aims to eliminate may be reintroduced. Here, we define a static taint analysis that targets both Rust and foreign code to detect the common memory errors use-after-free, never-free, and double-free, and implement it in the tool crema. Our experimental evaluation on real cases from GitHub shows that crema detects memory errors effectively.
As the capabilities and technologies of Unmanned Aerial Vehicles (UAVs) improve, new ways of utilizing them are being investigated. We investigate the use of reinforcement learning to navigate a UAV in an unknown environment, where the room layout is initially unknown. We present a novel approach for exploring and controlling a UAV, which must locate points of interest in such rooms. In this approach, we use reinforcement learning in an online fashion, meaning that the learning is performed multiple times as our knowledge of the room improves. We present the implementation of a stochastic model predictive control approach paired with Q-learning and partition refinement, using Uppaal Stratego to synthesize near-optimal strategies for UAVs to explore, map, and locate objects in environments with no prior knowledge. To ensure the safety of those strategies, we add a pre-shield during learning and employ a post-shield on the proposed actions to be executed. We evaluate our approach using simulation and compare it against a greedy approach, in which the UAV always visits the nearest unexplored part of the map. Our evaluation shows that the approach explores all points of interest approximately 11
This paper presents a Rodin plugin for automatically generating proof obligations for invariant preservation to ensure the correctness of an Algebraic State Transition Diagram (ASTD). ASTD is a graphical specification language that allows for the combination of Statechart-like extended hierarchical state machines using CSP-like process algebra operators. Invariants can be attached to any level in an ASTD to specify local properties. This plugin takes as input an ASTD in JSON format and produces the proof obligations within an Event-B context. It implements a formal approach that recursively generates all the proof obligations according to the structure of an ASTD. The tool currently supports automaton, sequence, guard and closure ASTDs, but can be easily extended to consider any ASTD type.
Software systems are composed of interacting processes that share data between each other in order to satisfy system properties. When these processes deviate and are unavailable to transmit data—due to events such as software bugs, hardware failures, or security attacks—a resilient system will continue delivering safety-critical services. Identifying the processes required to satisfy system properties is not a trivial task as there may exist multiple alternative dataflow paths that each satisfy the property. In this work, we propose a formal modeling and analysis technique to compute the sets of minimal processes required to satisfy dataflow properties. The computation of these sets is reduced to a maximum satisfiability problem via modeling in Alloy ^Max , a formal modeling language that performs bounded model checking. We then present a method to formally define the resilience criteria for a system by constraining the minimal dataflow required under maximum system deviations. The efficacy of this work is then evaluated with four case studies motivated from real-world systems with promising results.
Automotive architectures are evolving with increased computational power and network connectivity, including mandatory overthe- air updates. This transformation enlarges the attack surface and increases security risks that impact safety. This contribution investigates the security of automotive network architectures (ANAs) and application protocols via formal modeling and verification approaches. The focus is on resilience against a strong adversary that is capable of partial component and network compromise. The key questions that are addressed include the formal modeling of ANAs, the impact of compromised components, and the comprehensive evaluation of security properties (SPs). Attack Resilience Hyperproperties (ARHs) are introduced to model complex SPs that involve compromised components. A prototype tool, ExACT, is provided for the analysis of ARHs with the Tamarin Prover. Additionally, a scoring system is proposed to evaluate the robustness of architectural variants. The real-world applicability of these approaches is demonstrated through a case study involving an ANAs and a secure log file upload protocol.
In this invited talk, we will overview the application of various types of formal methods to optimize smart contracts and prove the correctness of the optimization results. Smart contracts are computer programs stored on a blockchain that are intended to automatically execute, control or document events and actions according to the terms of a contract or an agreement. The blockchain is one of the contexts in which the use of formal methods to enhance its security and efficiency is critical. On one hand, software bugs on smart contracts have already caused several high profile attacks and there is hence huge interest and investment in guaranteeing their correctness. Efficiency is of similar relevance as well, as deploying and executing smart contracts has a cost (in the corresponding cryptocurrency). Hence, optimization tools for smart contracts are emerging since the last few years. The talk will present our work on optimizing the efficiency of Ethereum smart contracts and ensuring the correctness of the optimization results. The basis of our work is the use of formal methods, including SAT and SMT solvers, proof-assistants, rule-based transformations, static analyses and greedy algorithms. Finally, we will also discuss the use of machine learning technology to boost the efficiency of our formal methods-based techniques.
In this paper, we tackle the reachability analysis problem of binary code that manipulate the part of memory that is just above the stack pointer. To model such programs, we use Upper Stack PushDown Systems (UPDS), an extension of Pushdown systems (PDS), to simulate the stack operations of assembly codes. UPDS is a kind of PDS with two stacks called upper stack and lower stack where the lower stack works as a normal PDS stack and the upper stack works as the memory space above the stack. We propose several algorithms to perform the reachability analysis of this model. To this aim, we represent regular potentially infinite sets of configurations using finite state automata. The reachability sets of UPDSs being in general not regular, we propose two semi-algorithms for computing accurately the sets of predecessors pre^* and successors post^* of regular sets of configurations of UPDS. We provide interesting subclasses for which our semi-algorithms are guaranteed to terminate. We show that our approach has several interesting applications like stack overflow detection, stack string detection, return address anomaly detection, etc.
Multi-objective probabilistic model checking is a powerful technique for verifying stochastic systems against multiple (potentially conflicting) properties. To enhance the trustworthiness and explainability of model checking tools, we present independently checkable certificates and witnesses for multi-objective ω-regular queries in Markov decision processes. For the certification, we extend and improve existing certificates for the decomposition of maximal end components and reachability properties. We then derive mixed-integer linear programs (MILPs) for finding minimal witnessing subsystems. For the special case of Markov chains and LTL properties, we use unambiguous Büchi automata to find witnesses, resulting in an algorithm that requires single-exponential space. Existing approaches based on deterministic automata require doubly-exponential space in the worst case. Finally, we consider the practical computation of our certificates and witnesses and provide an implementation of the developed techniques, along with an experimental evaluation, demonstrating the efficacy of our techniques.
Debugging and repairing faults when programs fail to formally verify can be complex and time-consuming. Automated Program Repair (APR) can ease this burden by automatically identifying and fixing faults. However, traditional APR techniques often rely on test suites for validation, but these may not capture all possible scenarios. In contrast, formal specifications provide strong correctness criteria, enabling more effective automated repair. In this paper, we present an APR tool for Dafny, a verification-aware programming language that uses formal specifications — including pre-conditions, post-conditions, and invariants — as oracles for fault localization and repair. Assuming the correctness of the specifications and focusing on arithmetic bugs, we localize faults through a series of steps, which include using Hoare logic to determine the state of each statement within the program, and applying Large Language Models (LLMs) to synthesize candidate fixes. The models considered are GPT-4o mini, Llama 3, Mistral 7B, and Llemma 7B. We evaluate our approach using DafnyBench, a benchmark of real-world Dafny programs. Our tool achieves 89.7
Students in computing education increasingly use large language models (LLMs) such as ChatGPT. Yet, the role of LLMs in supporting cognitively demanding tasks, like deductive program verification, remains poorly understood. This paper investigates how students interact with an LLM when solving formal verification exercises in Dafny, a language that supports functional correctness by allowing programmers to write formal specifications and automatically verifying that the implementation satisfies the specification. We conducted a mixed-methods study with master’s students enrolled in a formal methods course. Each participant completed two verification problems, one with access to a custom ChatGPT interface that logged all interactions and the other without. We identified strategies used by successful students and assessed the level of trust students place in LLMs. Our findings show that students perform significantly better when using ChatGPT; however, performance gains are tied to prompt quality. We conclude with practical recommendations for integrating LLMs into formal methods courses more effectively, including designing LLM-aware challenges that promote learning.
Formal verification has recently been increasingly used to prove the correctness and security of many applications. It is attractive because it can prove the absence of errors with the same certainty as mathematicians proving theorems. However, while most security experts recognize the value of formal verification, the views of non-technical users on this topic are unknown. We designed and implemented two experiments to address this issue to understand how formal verification impacts users. Our approach started with a formative study involving 15 participants, followed by the main quantitative study with 200 individuals. We focus on the application domain of Password Managers (PMs) since it has been documented that the lack of trust in PMs might lead to lower adoption. Moreover, recent efforts have focused on formally verifying (parts of) PMs. We conclude that formal verification is seen as desirable by users and identify three actionable recommendations to improve formal verification communication efforts.
The paper focuses on the convergence between artificial neural networks and biological neural systems, addressing the challenges of establishing a "morphic relation" between the two. The central problem lies in replicating biological neural networks' dynamic, adaptive, and self-organising properties within artificial constructs. Neuromorphic engineering (NE), an interdisciplinary field at the intersection of neuroscience and computer science, seeks to design artificial neural networks that emulate the structure, function, and temporal dynamics of biological systems. Although artificial neural networks have succeeded in areas like pattern recognition and natural language processing, they often need more fluid adaptability and robustness of biological systems. The paper explores recent advances in deep learning models, in particular deep neural networks, and their ability to capture structure-sensitive cognitive properties. Challenges remain despite promising findings, such as meta-learning techniques and systematic generalization. Deep neural networks, though efficient, often exhibit opaque and fragile learning mechanisms. The paper advocates further exploring the criteria to establish a genuine morphic relation between artificial neural networks and biological neural systems, focusing on structural, functional, and dynamic correspondences to advance the field of neuromorphic engineering.
In multi-agent systems, a particularly important action is that through which some agents share information with some others. Within epistemic logic and its relational semantics, this action has been represented as a model operation that assigns to every agent in the communicating group the relation describing the group's distributed knowledge in the initial model, leaving the relation of all other agents as before. While this approach works well when the shared information is knowledge, it has some issues when the shared information is beliefs: consistent agents might be turned into inconsistent ones. This manuscript explores an approach that relies on maximally consistent subgroups of agents, discussing also how to modify it to guarantee that all the relevant properties of beliefs are preserved.
The staggered model is a recent, very general variant of discrete-time quantum walks which, avoiding the use of a coin to direct the walker evolution, explores the underlying graph structure to build an evolution operator based on local unitaries induced by adjacent vertices. Optimising their implementation to increase resilience to decoherence phenomena motivates their analysis with the ZX-calculus. The whole optimisation can be seen as a graph reconfiguration process along which the original circuit is rewrote, significantly reducing the number of (expensive) gates used. The exercise identified an underlying pattern leading to an alternative, potentially more efficient evolution operator.
Switch graphs, as proposed by Marcelino and Gabbay are relation-changing state transition structures which make use of higher-level directed edges (edges connecting edges) to represent how the accessibility relation changes. In previous work, the same authors propose an hybrid logic to describe such systems. In this work we consider a variant of hybrid logic that excludes nominals and considers state-variables, and we explore how this logic can be used to describe these structures, in particular, higher-level edges. Afterwards, we define two classes of behavioural equivalence and discuss their utility and limitation with some examples.
