Static and dynamic program analysis techniques have been studied for several decades to provide foundations for tools that discover software defects or that verify their adherence to semantic properties. Applying these techniques to real-world programs presents several challenges, such as scalability and precision. This special issue of Software Tools for Technology Transfer comprises novel results and practical applications of these techniques. The papers in this special issue are extended versions of selected workshop papers from the proceedings of the 14th ACM SIGPLAN International Workshop on the State Of the Art in Program Analysis (SOAP 2025).
Abstract Across the broad research field concerned with analyzing computing systems, algorithms and tools revolve around the modeling languages used to describe the systems, hindering their applications to similar problems of systems in other modeling languages. For example, the research communities for formal verification and testing of hardware and software share common theoretical foundations and solving methods, including symbolic encoding, satisfiability solving, and abstraction refinement. Nevertheless, it requires significant effort for one community to benefit from the advancements of the other, as analyzers assume different modeling languages for input instances. To bridge the gap between hardware and software analysis, we propose Btor2C , a translator from word-level sequential circuits in the Btor2 language to C programs. We choose the Btor2 language as frontend because its simple syntax and bit-precise semantics make it a suitable intermediate representation for analysis purposes. Using Btor2C , we translate Btor2 circuits from the Hardware Model Checking Competitions into C programs and analyze them using tools from the Intl. Competitions on Software Verification and Testing. Our results show that software analyzers can complement hardware model checkers for enhanced quality assurance: Prominently, the software verifier Cbmc (with Btor2C for preprocessing) found more bugs than the best hardware model checkers ABC and AVR in our experiment.
Context-free language (CFL) reachability is a fundamental computational framework for formulating key static analyses (e.g., alias analysis, value-flow analysis, and points-to analysis) as well as some other graph analysis problems. Achieving high performance in universal CFL-reachability solvers remains a significant challenge. Specialized tools such as Pearl and Gigascale are optimized for specific CFLs but lack general applicability, whereas existing universal CFL-reachability solvers often do not scale well in important cases. In particular, prior efforts to leverage high-performance linear algebra operations in universal CFL-reachability solvers produced a matrix-based solver, MatrixCFPQ, that excels at performing common navigational queries on RDF graphs (which are unrelated to program analysis) but is inefficient when it comes to modeling static analyses. In this work, we introduce FastMatrixCFPQ, a universal matrix-based CFL-reachability solver that overcomes the limitations of MatrixCFPQ by leveraging the properties of the CFL-semiring, common patterns in context-free grammars, and the features of the SuiteSparse:GraphBLAS sparse linear algebra library. We prove that the optimized matrix-based algorithm for CFL-reachability has a worst-case running time of 𝒪(n^3) in the number of graph vertices n . Our experimental results demonstrate that FastMatrixCFPQ outperforms the state-of-the-art universal CFL-reachability solvers across five client analyses—often by orders of magnitude—and, in many cases, even surpasses the speed of specialized solvers designed for specific CFLs.
Chemical reaction networks (CRNs) are an established population model defined as a system of coupled nonlinear ordinary differential equations across many disciplines. In many applications, for example, in systems biology and epidemiology, CRN parameters such as the kinetic reaction rates can be used as control inputs to steer the system toward a given target. Unfortunately, the resulting optimal control problem is nonlinear, therefore, computationally very challenging. We address this issue by introducing an optimality-preserving reduction algorithm for CRNs. The algorithm partitions the original state variables into a reduced set of macro-variables for which one can define a reduced optimal control problem with provably identical optimal values. The reduction algorithm runs with polynomial time complexity in the size of the CRN. We use this result to reduce verification and control problems of large-scale vaccination models over real-world networks.
Given the increasing complexity and expanding frontiers of software systems during the last century, verification has become essential to ensuring reliability, security, and trustworthiness. The goal of the Challenges of Software Verification Symposium (CSV) is to monitor the state-of-the-art in this field, exploring challenges to this scientific discipline. This special issue of Software Tools for Technology Transfer presents novel theoretical directions and practical applications of these techniques. The papers in this special issue are extended versions of selected symposium contributions from the proceedings of the 4th Challenges of Software Verification Symposium, which took place at the Ca’ Foscari University of Venice, Venice, Italy, from June 5th and 6th, 2025.
In automotive engineering, vehicle platooning is a proposed method for improving convoy movements by coordinating them to increase the safety and efficiency of transportation systems. The complexity and stochastic nature of platooning systems provide difficulties for traditional model-checking techniques. However, Statistical Model Checking (SMC) offers a solution by using statistical inference to probabilistically evaluate system features. This paper shows that Uppaal SMC offers a robust framework for assessing platooning systems across various operational scenarios, combining statistical analysis and formal verification methodologies. The behaviour of the platoon is modelled stochastically to cover a wide range of driving scenarios and road surfaces. Using SMC, it has been possible to gauge the safety and functionality of the platoon by estimating the probability of several properties.
Developing large-scale collective adaptive systems for safety-critical applications requires an extensive effort, involving the interplay of distributed programming techniques and mathematical proofs of real-time guarantees. This effort could be significantly reduced by allowing the system developer to rely on libraries of predefined algorithms. By exploiting such algorithms, distributed behaviour and (hard) real-time guarantees for the final application could be automatically inferred, effectively shifting the verification burden from the system designer to the algorithm developer. Following earlier work on real-time guarantees for aggregate computing algorithms, we argue that aggregate computing could provide a convenient framework towards this aim. As a first step, we give a detailed description of different kinds of models that can interpret corresponding classes of aggregate programs as mathematical functions. Then, building on such models, we investigate the problem of how real-time behaviour constraints can be specified in a compositional way, proposing a few composable specification patterns, and singling out a number of potential building block library algorithms that could constitute such a real-time aggregate computing library. We evaluate our proposal by means of examples, describing a series of example algorithms for each proposed model, and by investigating two possible compositions of some of them in an archetypal scenario of distributed estimation of the network diameter. In these two examples, we experimentally prove the effectiveness of the models by comparing the results of the interpretation with the simulations results, achieving a close match. Overall, the proposed framework provides a roadmap towards a real-time aggregate computing library with the potential of providing a valuable asset for supporting the rigorous engineering of safety-critical large-scale collective adaptive systems.
Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today's state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners-tool builders and users alike.
The rapid progress of quantum technologies, fostered by the efforts of both academia and industry, has stimulated the design of quantum programming languages and the development of methods to support their verification and optimization. As in the classical setting, static analysis plays a fundamental role in such an endeavour. In this paper, we provide a survey on static analysis approaches for quantum programs, which have been proposed in the literature, distinguishing between dataflow-oriented approaches, which are based on a graph representation of the program information flow, and domain-oriented approaches, which essentially consist of the definition of some appropriate abstract domains representing the program property to be analysed. To illustrate these two perspectives concretely, we also present in detail two specific analyses: a dataflow analysis for managing quantum variables and uncomputation, and a static analysis based on abstract interpretation for detecting state entanglement.
Model checking undiscounted reachability and expected-reward properties on Markov decision processes (MDPs) are key for the verification of systems that act under uncertainty. Popular algorithms are policy iteration and variants of value iteration; in tool competitions, most participants rely on the latter. These algorithms generally need worst-case exponential time. However, the problem can equally be formulated as a linear programme, solvable in polynomial time. In this paper, we give a detailed overview of today’s state-of-the-art algorithms for MDP model checking with a focus on performance and correctness. We highlight their fundamental differences, and describe various optimizations and implementation variants. We experimentally compare floating-point and exact-arithmetic implementations of all algorithms on three benchmark sets using two probabilistic model checkers. Our results show that (optimistic) value iteration is a sensible default, but other algorithms are preferable in specific settings. This paper thereby provides a guide for MDP verification practitioners—tool builders and users alike.
The weakest precondition (WP) of a program describes the largest set of initial states from which all terminating executions of the program satisfy a given postcondition. The generation of WPs is an important task with practical applications in areas ranging from verification to run-time error checking. This paper proposes the combination of Large Language Models (LLMs) and fuzz testing for generating WPs. In pursuit of this goal, we introduce Fuzzing Guidance (FG); FG acts as a means of directing LLMs towards correct WPs using program execution feedback. FG utilises fuzz testing for approximately checking the validity and weakness of candidate WPs, this information is then fed back to the LLM as a means of context refinement. We demonstrate the effectiveness of our approach on a comprehensive benchmark set of deterministic array programs in Java. Our experiments indicate that LLMs are capable of producing viable candidate WPs, and that this ability can be practically enhanced through FG.
We present an empirical study on the ability of Large Language Models (LLMs) to understand code by detecting semantically equivalent and inequivalent programs, that is, whether they compute the same result given the same input or not. To probe this, we deliberately perturb the program text by introducing semantics-preserving code transformations, namely copy propagation and constant folding. Using a benchmark of 11 Python functions with both equivalent and non-equivalent variants, we evaluate seven state-of-the-art LLMs (including ChatGPT, Claude, Gemini, and Deep-Seek) under zero-shot prompting, with and without minimal context. Despite strong performance in code generation tasks, the models often fail in this deeper reasoning challenge, misclassifying 41
Autonomous multi-agent systems use different modes of communication to support their autonomy and ease of interaction. In order to enable modelling and reasoning about such systems, we need frameworks that combine many forms of communication. R-CHECK is a modelling, simulation, and verification environment supporting the development of multi-agent systems, providing attributed channelled broadcast and multicast communication. Another common communication mode is point-to-point, wherein agents communicate with each other directly. Capturing point-to-point through R-CHECK’s multicast and broadcast is possible, but cumbersome and prone to interference. Here, we extend R-CHECK (and its underlying formal calculus ReCiPe) with bidirectional attributed point-to-point communication, which can be established based on identity or properties of participants. Moreover, we provide a compositional semantics that clearly describes how different modes of interaction co-exist without interference. We also support model-checking of point-to-point interactions by extending linear temporal logic with observation descriptors related to the participants in this communication mode. We argue that these extensions simplify the design, and demonstrate their benefits by means of an illustrative case study.
Event-driven programming provides a natural fit for the reactive nature of pervasive systems like the Internet of Things (IoT) and Collective Adaptive Systems (CASs). Attribute-based memory Updates (AbU) is a calculus based on Event-Condition-Action (ECA) rules, well-suited for modeling such decentralized systems. This paper introduces a novel extension of AbU by incorporating ECA rule priorities. We show how this extension facilitates the natural expression of prioritized behaviors and enables the implementation of distributed data structures like Conflict-free Replicated Data Types (CRDTs). Furthermore, by leveraging the local invariants of AbU nodes and priorities we address the problem of enforcing global invariants in order to enhance the reliability and predictability of CASs. This is achieved through a syntactic transformation that projects global invariants into local ones and introduces high-priority synchronization rules, so that system-level properties can be guaranteed without relying on a central authority.
Agent behavior is shaped by latent decision parameters that govern how rewards are interpreted and traded off over time. A key example is the discount factor, which encodes time preference. Mis-specifying the discount factor can confound reward-centric behavioral models (e.g., inverse RL), motivating the need to infer time preference directly from behavior. This paper presents methods for discount factor elicitation in finite-state Markov Decision Processes via policy observations and controlled reward modifications. First, we introduce an algorithm that bounds the set of discount factors consistent with an agent’s observed (near-)optimal policy, and show how observations across heterogeneous reward settings progressively tighten these bounds. Building on this result, we propose an active elicitation framework in which an ego agent strategically adjusts rewards (with fixed dynamics) to refine its estimate of another agent’s discount factor. Through case studies, we demonstrate that active elicitation accelerates interval refinement relative to passive observation and enables targeted exploration in strategic multi-agent settings. Overall, our results establish reward modification as a principled mechanism for eliciting discount factors and improving behavioral modeling, prediction, and control.
This special issue of the International Journal on Software Tools for Technology Transfer presents extended versions of four selected papers from QEST+FORMATS 2024, the first joint edition of the International Conference on Quantitative Evaluation of Systems (QEST) and the International Conference on Formal Modeling and Analysis of Timed Systems (FORMATS). The joint conference was held in Calgary, Canada, in September 2024. The papers provide a compact snapshot of current directions in quantitative evaluation and timed systems research.
Epistemic ensembles are systems of knowledge-based agents capable of accessing, sharing, and updating information about themselves and their peers. These agents can operate on shared or local epistemic states through actions that dynamically alter the knowledge of some or all members of the ensemble. To support abstract reasoning over such systems, we introduce the notion of focus set — a selected set of logical formulæ that provide an abstraction from the underlying system state. Based on this abstraction, we define global and distributed symbolic representations of epistemic states, along with representable epistemic actions that enable efficient symbolic updates. For formal analysis, we define a generic operational semantics and develop and relate three complementary semantic frameworks: (1) a semantic environment, where system states are modelled as epistemic states, (2) a symbolic environment, where knowledge is represented as sets of logical formulæ, and (3) a distributed environment, represented by a family of local knowledge bases where each agent has its own local symbolic state. We establish a correspondence between these environments via a notion of relative elementary equivalence. Our main result demonstrates that equivalent configurations simulate each other’s behaviour and satisfy the same dynamic epistemic formulæ, ensuring representational consistency across all three perspectives. This provides a robust foundation for reasoning about distributed knowledge and belief dynamics in cooperative multi-agent systems.
Quantitative monitoring mitigates two issues observed in exhaustive, qualitative verification approaches, namely the state-space explosion problem and the rigidity of their binary verdicts. This is achieved through (i) analysing individual executions instead of building the whole state-space and (ii) providing a robustness measure instead of yes/no answers. In this paper, we consider real-time systems where executions and specifications are modelled as timed signals and Signal Temporal Logic (STL) formulae, respectively. We propose a new temporal robustness measure δ for STL, based on a new distance that we define over timed signals. In contrast with existing measures, δ provides a precise quantification of distances between the monitored signal and the boundary separating faulty and non-faulty executions w.r.t. an STL property. Thus, δ is suitable for a wide range of real-life perturbations, such as those affecting exclusively a particular time window within a signal. Though we prove that computing δ is NP-hard in general, we provide efficient algorithms for a practical fragment of STL. In particular, this fragment includes the key property of bounded response. This paper is an extension of (Rino et al. in Joint International Conference on Quantitative Evaluation of SysTems International Conference on Formal Modeling and Analysis of Timed Systems (QEST+FORMATS), 2024), published at QEST+FORMATS 2024. The extension includes implementation of algorithms to compute δ in a prototype tool, and an evaluation of our approach on a case study of quality assessment of insulin controllers for diabetic patients.
Process mining is concerned with deriving formal models capable of reproducing the behaviour of a given organisational process by analysing observed executions collected in an event log. The elements of an event log are finite sequences (called also traces or words) of actions. Many effective algorithms have been introduced which issue a control flow model (commonly in Petri net form) aimed at reproducing, as precisely as possible, the language of the considered event log. However, given that identical executions can be observed several times, traces of an event log are associated with a frequency and, hence, an event log inherently yields also a stochastic language. By exploiting the trace frequencies contained in the event log, the stochastic extension of process mining, therefore, consists in deriving stochastic (Petri net) models capable of reproducing the likelihood of the observed executions. In this paper, we introduce a novel stochastic process mining approach. Starting from a non-stochastic Petri net model mined through classical mining algorithms, we employ optimization to identify optimal weights for the transitions of the mined net so that the stochastic language issued by the stochastic interpretation of the mined net closely resembles that of the event log. The optimization is either based on the maximum likelihood principle or on the earth moving distance and we study in detail the characteristics of the associated objective function in both cases. It turns out that the objective function in case of using the maximum likelihood approach lends itself better to optimization. Experiments on some popular real system logs show an improved accuracy with respect to alternative approaches.
Micro-Stipula is a stateful calculus in which clauses can be activated either through interactions with the external environment or by the evaluation of time expressions. Despite the apparent simplicity of its syntax and operational model, the combination of state evolution, time reasoning, and nondeterminism gives rise to significant analytical challenges. In particular, we show that determining whether a clause is never executed is undecidable. We formally prove that this undecidability result holds even for syntactically restricted fragments: namely, the time-ahead fragment, where all time expressions are strictly positive, the instantaneous fragment, where all time expressions evaluate to zero, and the determinate fragment, where the initial states of functions and events are disjoint. On the other hand, we identify a decidable subfragment: at the intersection of the instantaneous and determinate fragments reachability becomes decidable.
