With the advancement of neural networks, neural network controlled systems (NNCSs) are increasingly deployed in safety-critical scenarios, making the safety verification of NNCSs imperative. Traditional verification methods based on overapproximated reachability analysis introduce precision loss during the verification process, which may lead to “Unknown” results. Moreover, standalone forward reachability analysis often fails to incorporate target safety properties into its verification process, while backward reachability analysis does not account for input constraints. To address these challenges, this paper proposes an iterative refinement approach by combining forward and backward reachability analysis. For a given safety property, our method guides state space partitioning and pruning on-the-fly by making use of the target safety constraints when verification results remain “Unknown”. By partitioning the state space into smaller subspaces, the precision loss due to overapproximation is significantly mitigated. Additionally, integrating forward and backward reachability analysis further counteracts these overapproximation effects through pruning, ultimately yielding more accurate verification outcomes. We demonstrate that our approach successfully verifies the system's safety properties with a 100% success rate across four benchmarks, whereas other verification tools for NNCSs such as Reach-LP-GSG, BReach-LP, and DRIP-Hpoly either return “Unknown” results or require up to$29 \%, 60 \%$, and 232% more time.

Neural network verification, particularly verification of robustness properties, has received much research attention. However, many existing verification methods overlook the influence of floating-point rounding errors in the deployed neural networks, resulting in unsound verification outcomes. In this paper, we propose a sound robustness verification approach aiming at overcoming this limitation. Our method utilizes real-number intervals to approximate floating-point arithmetic and abstracts floating-point neural networks into equivalent networks using real-number interval arithmetic semantics, thereby effectively taking into account for floating-point rounding errors. We sub-sequently employ exact MILP formulations to verify robustness over these abstracted networks. We introduce FMIPVerify, a dedicated verification tool tailored to ensure the soundness of floating-point neural network verification. Experimental results demonstrate that FMIPVerify significantly improves the robustness verification ability in floating-point ReLU neural networks compared to established complete methods like MIPVerify.

Recognizing defects in source code through deep learning methods has become an important research subject for improving software quality. Although Transformer-based models such as CodeBERT have demonstrated impressive performance improvement in defect prediction tasks, models relying on single-structured input data, such as sequences, have limited ability to capture the code's structural features. Treating code simply as text overlooks essential information such as control dependencies, data dependencies, and syntactic structures inherent in the code. This paper proposes the Heterogeneous Discrete Code Graph (HDCG), which assigns structural information to code tokens from multiple perspectives. We also introduce an improved transformer model FINEGATE that leverages HDCG to guide self-attention. The experiments demonstrate that FINEGATE can effectively predict source code defects and perform fine-grained defect localization.

In scientific computation, developers usually exploit the compiler to improve the performance of floating-point programs. However, many compiler optimizations might affect the floating-point behavior, which can cause numerical variations. This paper proposes an efficient generation method of floating-point inputs for compiler-induced variability. Specifically, we formulate the problem of generating high variability-inducing inputs as a mathematical optimization problem and solve it through input space partition and Markov Chain Monte Carlo (MCMC) sampling. To improve the sampling efficiency, besides the result variation, we utilize the difference between the execution traces of floating-point instructions to guide the search. We have implemented our approach in the tool CIV. Compared to the state-of-the-art method, CIV achieves an average 11x speedup for generating an equivalent or better input to trigger large result variations. Moreover, CIV finds better inputs for 100% programs and has better stability for detecting large result variations. The experimental results demonstrate the effectiveness and efficiency of our approach.

F1oating-point numbers use limited precision to represent real numbers and have rounding errors, so floating-point calculations are inherently inaccurate. Revealing high floating-point errors is critical to software safety. Recently, two representative testing approaches, DEMC and ATOMU, have been proposed to find inputs triggering high floating-point errors in numerical programs. However, DEMC does not process the entire input domain and suffers from the high search cost, while ATOMU may get trapped in a local maximum. In this paper, we propose a novel approach that combines ranking analysis and search algorithms to detect high floating-point errors in numerical programs. The key idea is to use ranking analysis over the input domain to reduce search space quickly, and exploit search algorithms to find the inputs that may trigger high floating-point errors. We have implemented our approach and evaluated it on 88 numerical programs in GNU Numerical Library(GSL). The experimental results demonstrate our approach can find more high floating-point errors compare to ATOMU and DEMC. Moreover, our approach achieves 14× and 4× improvement in detecting higher floating-point errors compare to ATOMU and DEMC, respectively. As a black-box method, RADE achieves a 5. 25× speedup compared to DEMC which is the state-of-the-art black-box method.

The Message Passing Interface (MPI) is the standard paradigm of programming in high performance computing. However, the inherent complexity and the large size of MPI standard make it difficult for programmers to use the MPI APIs correctly. This paper focuses on the mismatch errors of message signatures. Considering that MPI errors may occur during some intricate, low probability interleavings under specific inputs, we adopt symbolic verification to verify the correct match of message signatures. Specifically, we propose a precise method for modeling the match of message signatures of an execution path in terms of communicating sequential processes. To improve the scalability, we give a partial order reduction based optimization to reduce the complexity of path-level communication models. We have implemented our method as a prototype tool and evaluated it on the typical correctness benchmark MPI-Corbench and 8 real-world open source MPI programs, totaling 37K lines of code. The experimental results demonstrate the effectiveness and scalability of our method.

Safety and robustness properties are highly required for neural networks deployed in safety-critical applications. Current complete verification techniques of these properties suffer from the lack of efficiency and effectiveness. In this article, we present an efficient complete approach to verify safety and robustness properties of neural networks through incrementally determinizing activation states of neurons. The key idea is to generate constraints via layerwised splitting that make activation states of hidden neurons become deterministic efficiently. These constraints are then utilized for refining inputs systematically so that abstract analysis over the refined input can be more precise. Our approach decomposes a verification problem into a set of subproblems via layerwised input space splitting. The property is then checked on each subproblem, where the activation states of at least one hidden neurons will be determinized. Further checking is accelerated by constraint-guided input refinement. We have implemented a parallel tool called LayerSAR to verify safety and robustness properties of ReLU neural networks in a sound and complete way, and evaluated it extensively on several benchmark sets. Experimental results show that our approach is promising, compared with complete tools, such as Planet, Neurify, Marabou, ERAN, Venus, Venus2, and nnenum in verifying safety and robustness properties on the benchmarks.

Analyzing worst-case resource usage of a program is a difficult but important problem. Existing static bound analysis techniques mainly focus on deriving the upper-bound number of visits to a given control location or iterations of a loop. However, there still exist gaps between such bounds and resource usage bounds. In this paper, we present a static analysis approach to derive resource usage bounds for imperative programs. We leverage techniques of program transformation, numerical value analysis, pointer analysis and program slicing, to model and analyze resource usage in a program. We have conducted experiments to derive usage bounds of various resources in C programs, including heap memory, file descriptors, sockets, user-defined resources, etc. The result suggests that our approach can infer usage bounds of resources in practical imperative programs.

It is widely desired to precisely predict bounds of resource usages statically in a program, particularly when the program runs in resource-limited contexts. The resource bound problem becomes more challenging for C programs due to the allowed flexible manipulations on dynamically allocated resources in C. In this paper, we present a static analysis approach to deriving the bounds of dynamically allocated resources for C programs. The key idea is to combine numerical value analysis with pointer analysis under the unified framework of abstract interpretation. First, to track resource usage, we intro-duce auxiliary numerical variables to model the resource usage due to resource-manipulating functions such as allocation and deallocation. Second, to handle resource-manipulating functions involving pointers as parameters or return values, we propose a pointer analysis approach designed specifically for resource bound analysis, and combine it with numerical value analysis, to handle pointer arithmetics, dynamic allocation and deallocation, etc. Then, we infer the value bound of auxiliary resource-usage modeling variables to predict resource bounds at each program location. We have implemented our approach in a tool called DARB and conducted experiments on a set of benchmarks extracted from real-world programs. The results show that DARB can deal with C programs with complex resource manipulations.

The classic linear (technically, affine) equality abstract domain, which can infer linear equality relations among variables of a program automatically, is one of the earliest and fundamental abstract domains. As a lightweight relational abstract domain, it has been widely used in program analysis. However, it cannot express non-convex properties that appear naturally due to the inherent disjunctive behaviors in a program. In this paper, we introduce a new abstract domain, namely the abstract domain of linear absolute value equalities, which generalizes the linear equality abstract domain with absolute value terms of variables. More clearly, we leverage the absolute value function to design the new abstract domain for discovering linear equality relations among values and absolute values of program variables. The new abstract domain can be used to infer piecewise linear behaviors (e.g., due to conditional branches, absolute value function calls, max/min function calls, etc.) in a program. Experimental results of our prototype are encouraging: In practice, the new abstract domain can find interesting piece-wise linear invariants that are non-convex and out of the expressiveness of the linear equality domain.

Numerical computation is often involved in software of embedded control systems, cyber-physical systems, artificial neural network systems, big data processing systems, etc. Automatically discovering numerical loop invariants is fundamental for checking the safety of such software. Abstract interpretation provides a framework to automatically discover sound invariants but which may be not precise enough due to over-approximations. One major source of precision loss is due to the limited linear expressiveness of most widely used numerical abstract domains and the widening operation. This becomes more serious when analyzing all variables simultaneously as a whole for programs that involve nonlinear behaviors. Based on the observation that the dependency among variables in a loop can be hierarchical, in this article, we propose a hierarchical static analysis to analyze a loop by utilizing relaxed abstract transformers. The main idea is to first partition all variables involved in a loop into different hierarchical layers, then compute invariants over the variables layer by layer in a bottom-up manner. During the iterative process, the computed invariants over lower layer variables are then used to relax transfer functions when analyzing the higher layer variables. One benefit of our method lies in that it can generate linear invariants to soundly enclose nonlinear behaviors in a loop. Finally, we present encouraging experimental results on benchmark programs involving nonlinear behaviors.