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.

Abstract VeriAbs is a strategy selection-based reachability verifier for C programs. The selection of a suitable strategy is from a pre-defined set of strategies and by taking into account the syntax and semantics of the code to be verified. This year we present VeriAbs version 1.4.1 in which a novel preprocessor to strategy selection is introduced. The preprocessor checks for the feasibility of performing a lightweight slicing of the input code using function call graph and variable reference information. By this if the program is found to besliceable, sub-programs or slices are generated, and the known strategy selection algorithm of VeriAbs is applied to each slice. The verification results of each slice are then composed to derive that of the entire program. This compositional verification has improved the scalability of VeriAbs and presented in this paper.

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.

Static analysis of code is very effective in finding common programmer errors but it comes at a price - a large number of false positives. Model checking, on the other hand, is very precise but does not scale up. We have developed a tool that combines both techniques and also implements a novel loop abstraction. The tool was run on 2 million lines of embedded code to analyze for two properties - division by zero and array index out of bounds. In other experiments we compared the precision of our tool to that achieved by tools implementing abstract interpretation. This paper presents details of the tool and the results of evaluations that we have carried out to measure the scalability and to compare the precision of our method on industry code against other static analysis tools.