Verification tools and techniques are known to possess strengths and weaknesses with respect to different program syntax and semantics. Thus in practice, a sequence of verification techniques is often custom built to verify a class of similar programs. Such a sequence of techniques is called a strategy. So far, verification strategies have been created manually or through machine learning methods. Manual methods of strategy creation are expensive. They create few strategies from which a suitable one is selected for a given program based on its class. The program's class is identified by observing the status of a few manually defined boolean program features. On the other hand, machine learning methods rely on a relatively large set of complex features such as program construct counts, ratios of construct counts or program graphs. In this paper we utilize a machine learning approach to create strategies. This approach combines the strengths of both previously known methods. It uses boolean program features with machine learning to predict verification strategies. Further, we introduce novel program features termed as relative boolean metrics that are boolean abstractions of ratios of construct counts. We implement the novel methods in a tool, extensively evaluate it on a large set of diverse academic benchmarks, and use it to verify four industrial applications. On an average our tool leads the state of the art manual and machine learning-based strategy prediction methods by 11% in terms of the number of properties it successfully verified.

Reactive systems, designed for embedded applications, commonly feature an outer infinite loop that captures environmental input and according to the inputs decides the system’s response. The outer infinite loop implies that almost every reactive system contains nested loops. Existing verification techniques, such as model checking and loop abstraction methods, often struggle in terms of accuracy and efficiency in the presence of nested loops. This paper presents an abstraction approach called outer loop abstraction or OLA targeting nested loops. It selectively abstracts outer loops which infinitely read and process environmental input, transforms the input code, and passes it on to any existing industrial verifier to proceed with verification. Our proposed approach facilitates efficient and scalable verification of input properties through model checking. This technique complements existing slicing and abstraction techniques and has demonstrated promising results when applied to an industrial verifier.

Abstract We present VeriAbsL, a reachability verifier that performs verification in three stages. First, it slices the input code using a combination of two slicers, then it verifies the slices using predicted strategies, and at last, it composes the result of verifying the individual slices. We introduce a novel shallow slicing technique that uses variable reference information of the program, and data and control dependencies of the entry function to generate slices. We also introduce a novel strategy prediction technique that uses machine learning to predict a strategy. It uses boolean features to describe a program to a neural network that predicts a strategy. We use the portfolio of VeriAbs, a reachabiltiy verifier with manually defined strategies. In sv-comp 2023, VeriAbsL verified 227 (Without witness validation.) more programs than VeriAbs, and 475 (Without witness validation.) programs that VeriAbs could not verify.

Modern software verification tools are moving towards incremental verification of program properties to ensure safety of evolving software systems. These tools analyze each and every change in the code. However, not every change in the program impacts verification outcome of program properties. Moreover, analyzing these irrelevant changes adds to cost of incremental verification. To address this, we are proposing a light-weight pre-analysis phase that identifies relevant changes with respect to program properties before applying any incremental verification technique. To identify such relevant changes, we present the Relevant Change Identification Technique (RCIT). RCIT uses a variant of the Strongly Live Variables (SLV) analysis to compute variables that are influencing the verification outcome of program properties. RCIT, then uses these variables to identify relevant changes. We evaluated RCIT on the changes made in five versions of open source applications with respect to two type of program properties - array index out of bound and zero division. RCIT identifies 59% of the actual changes as irrelevant.

Static analysis tools, being scalable, are widely used to detect runtime errors in industry strength software. However, the downside is that these tools generate a large number of false alarms which considerably reduces their effectiveness in detecting the real bugs and fixing them. This shortcoming becomes more pronounced in analysis of evolving software where false alarms reported in an earlier version are re-reported while analysing subsequent versions. Ideally, developers would not like to see the re-reporting of old alarms that are inconsequential to the changes made. To address this problem, static analyzers have been enhanced with techniques like syntactic masking, and several heuristics to decide if an old alarm should be reported again or not. Naturally, however, as they do not take semantics of change into consideration, they are either unsound, or still end up reporting a large number of old alarms. This paper proposes a change-based alarm reporting approach, that reports an alarm only if the alarm point lies on a newly introduced, potentially unsafe, execution path. For this, we intro-duce a novel and effective semantic-aware change-impact analysis (CIA), that helps in detecting presence of such execution paths. In order to make this efficient, especially for development processes involving frequent code commits, our technique incrementally builds the required dataflow analyses and program dependence information. Our experiments, on 124 versions of a core banking application, demonstrate that the proposed approach is i) 66% faster than whole program analysis, ii) leads to 83% reduction in repetitive alarms, and iii) reports 62% lesser alarms as compared to syntactic CIA.

K-limited path-sensitive interval domain is an abstract domain that has been proposed for precise and scalable analysis of large software systems. The domain maintains variables’ value ranges in the form of intervals along a configurable K subsets of paths at each program point, which implicitly provides co-relation among variables. When the number of paths at the join point exceeds K, the set of paths are partitioned into K subsets, arbitrarily, which results in loss of precision required to verify program properties. To address this problem, we propose selective merging of paths - identify and merge paths in such a way that the intervals computed help verifying more properties. Our selective path-sensitive approach is based on the knowledge of variables whose values influence the verification outcomes of program properties. We evaluated our approach on industrial automotive applications as well as academic benchmarks. We show benefits of selective path merging over arbitrary path selection by verifying 40% more properties.

Abstract VeriAbs is a strategy selection based reachability verifier for C code. It analyzes the structure of loops, and intervals of inputs to choose one of the four verification strategies implemented in VeriAbs. In this paper, we present VeriAbs version 1.4 with updates in three strategies. We add an array verification technique called full-program induction, and enhance the existing techniques of loop pruning, k-path interval analysis, and disjunctive loop summarization. These changes have improved the verification of programs with arrays, and unstructured loops and unstructured control flows.

Verification of programs continues to be a challenge and no single known technique succeeds on all programs. In this paper we present VeriAbs, a reachability verifier for C programs that incorporates a portfolio of techniques implemented as four strategies, where each strategy is a set of techniques applied in a specific sequence. It selects a strategy based on the kind of loops in the program. We analysed the effectiveness of the implemented strategies on the 3831 verification tasks from the ReachSafety category of the 8th International Competition on Software Verification (SV-COMP) 2019 and found that although classic techniques - explicit state model checking and bounded model checking, succeed on a majority of the programs, a wide range of further techniques are required to analyse the rest. A screencast of the tool is available at https://youtu.be/Hzh3PPiODwk.

Efficient automatic verification of real world embedded software with numerous properties is a challenge. Existing techniques verify a sufficient subset of properties by identifying implication relations between their verification outcomes. We believe this is expensive and propose a novel complementary approach called grouping. Grouping does not consider the verification outcomes but uses data and control flow characteristics of the program to create disjoint groups of properties verifiable one group at a time.We present three grouping techniques, a framework, and experiments over open source and industrial applications to support our thesis. The experiments show a high gain in performance of a few state-of-the-art tools. This led to the integration of grouping into the verification process of an automotive software manufacturer.

Loop Abstraction followed by Bounded Model Checking, or LABMC in short, is a promising recent technique for proving safety of large programs. In an experimental setup proposed last year [14], LABMC was combined with slicing and Iterative Context Extension (ICE) with the aim of achieving scalability over industrial code. In this paper, we address two major limitations of that set-up, namely (i) the inability of ICE to prune redundant code in a verification context, and (ii) the unavailability of a tool that implements the set-up. We propose an improvement over ICE called Iterative Function Level Slicing (IFLS) and incorporate it in our tool called ELABMC, to offer an efficient implementation of [14]. We substantiate our claim with two sets of experiments over industrial applications as well as academic benchmarks. Quantifying the benefits of IFLS over traditional ICE in one, our results report that IFLS leads to 34.9% increase in efficiency, 17.7% improvement in precision, and scales in 14.2% more cases. With the second experiment, we show that ELABMC outperforms state-of-the-art verification techniques in the task of identifying static analysis warnings as false alarms.

Abstract interpretation is widely used to perform static code analysis with non-relational (interval) as well as relational (difference-bound matrices, polyhedral) domains. Analysis using non-relational domains is highly scalable but delivers imprecise results, whereas, use of relational domains produces precise results but does not scale up. We have developed a tool that implements K-limited path sensitive interval domain analysis to get precise results without losing on scalability. The tool was able to successfully analyse 10 million lines of embedded code for different properties such as division by zero, array index out of bound (AIOB), overflow-underflow and so on. This paper presents details of the tool and results of our experiments for detecting AIOB property. A comparison with the existing tools in the market demonstrates that our tool is more precise and scales better.