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).
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.
