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.

Model checking engines employed to generate test cases covering the structure of the model or code are limited by factors like code size, loops and floating point computation. We propose an approach that overcomes these limitations by approximating code fragments by dynamically inferring their post-conditions. We use Daikon to infer likely invariants from execution traces, which are used as postconditions to compactly represent the state space computed by these code fragments. The resulting approximation enables application-level test case generation over larger code sizes using model checking, given the same resources of time, memory and computing power. Case studies show the efficacy of this approach.

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.