Software and Computational Systems Lab

Value analysis [1] is one verification technique in the software analysis framework CPAchecker [2], which tracks the concrete values of certain variables that are determined by its precision. So far, value analysis may create an empty initial precision or an initial precision from an existing value or predicate precision, which in both cases is the result of a previous analysis run. This restricts the reuse of information in the value analysis. The goal of this thesis is to extend the ability of CPAchecker's value analysis to reuse information from previous analysis runs by using information provided in YML correctness witnesses [3]. The idea is to derive from the invariants in the witness the variables that should be tracked and add them to the precision. In addition to considering variables directly occurring in the witness' invariant, further variables might be derived similar to [4]. An experimental evaluation should evaluate the value of generating initial precisions from witnesses. The evaluation should at least compare initial precision from witnesses generated by the value analysis with initial precision from value precision in context of the reverification of changed programs and optionally of the same program. The evaluation may be extended by a comparison with an initial empty precision as well as a precision from predicate analysis, an initial precision from witnesses generated from other analyses like CPAchecker's predicate analysis, k-induction, or even generated by another tool. Similar to [4], the evaluation may further evaluate the approach in context of cooperative verification.

Test-case generation based on reachability analyses like CoVeriTest [1] check the reachability of each test goal, e.g., each branch of a program, and generate a test case whenever the check succeeds. The goal of this thesis is to develop an approach to parallelize such test-case generation approaches by splitting the set of test goals into disjoint subsets and then running multiple instances of the test-case generation in parallel, each instance focusing on one particular subset of the test goals. The main conceptual part of the thesis is the development of one or more split strategies. Ideally the strategies should consider dependencies, e.g., dominator information or control-dependencies [2], or other structural relations between test goals. In addition, a baseline strategy, e.g., random splitting, should be provided. Since a test case may cover more than the test goal it is generated for, the parallelization approach should also support to exchange information about covered test goals to avoid generating test cases for already covered test goals. Ideally, the developed approach would support load balancing, i.e., the redistribution of uncovered test goals from one instance of the test-case generation approach to another one. The developed approach must be integrated into CPAchecker's [3] test-case generation and experimentally evaluated on the benchmarks of the international testing competition (Test-Comp) [4]. The evaluation must compare the approach to sequential test-case generation and compare the different strategies.

Software testing is a standard means in quality assurance supported e.g., by automatic tools for test input generation. Several of these automatic tools generate test suites aiming at maximizing the value wrt. a coverage criterion like branch coverage. One particular class of tools are test-case generators based on model checkers like CPAchecker [1,2,3]. These tools derive test goals from the coverage criterion (e.g., the set of branches in a program) and show the reachability of each goal to derive tests. Often, one generated test can reach more than the test goal it was created for. While it is easy to detect other test goals that were visited before reaching the test goal of interest and model-checking based test-case generators often would have covered those test goals with a previous test anyways, other test goals visited after reaching the test goal need to be explicitly determined. The goal of this thesis is to apply CPAchecker's value analysis [2] to determine test goals reached after the test goal of interest with the test inputs generated from showing the reachability of that test goal and integrate this procedure into CPAchecker's test-case-generation algorithm. Ideally, the value analysis should start after the test goal of interest, but could also start from the beginning with the test. In both cases, the value analysis needs to be configured to follow the path induced by the generated test and the visited test goals must be extracted from the path and marked as covered. In the former case, the initial state for the value analysis needs to be derived from the path reaching the test goal and the analysis needs to stop if a new input is required or the analysis cannot precisely determine a branch direction. In the latter case, the value analysis needs to read the test inputs and the analysis needs to stop if a new input is required but no further input is provided by the test or the analysis cannot precisely determine a branch direction. The tasks of the thesis is to design a concept for the detection approach and its integration into CPAchecker's test-case-generation procedure. The designed approach should be implemented in CPAchecker. Also, its efficiency and effectiveness should be evaluated. For example, one could compare the CPU time, number of covered test goals, and number of generated tests using one or more of CPAchecker's test-case generation configurations with and without the detection approach on the Test-Comp benchmark [4].

To evaluate the test generation tools participating in the International Competition on Testing, the validator executes the generated tests and measures coverage or reachability of a particular method call. For a reliable validation, i.e., test execution, all variables in a test task (C program plus coverage property) need to be properly initialized before influencing the observable program behavior (i.e., program control flow our output) or simplified before read for the first time. Per rule definition, variables should be initialized with __VERIFIER_nondet_XXX calls. In a first step, this thesis shall analyze the test tasks of the competition (a subset of the software verification competition benchmark [1]) for both categories coverage branches and coverage error-call to detect uninitialized variables usages. To this end, one may compile the programs with clang, gcc, etc. using particular compiler flags for uninitialized variables, apply a static analyzer, or run the validator with (a subset of the) tests generated in the last edition of the competition and dynamically observe uninitialized variable usages for instance with Valgrind [2]. Before one decides for one or multiple of these techniques, one should compare what kind of uninitialized variables the approaches detect, e.g., only uninitialized on some paths, uninitialized array entry, uninitialized memory, etc. In a second step, the uninitialized variable usages should be fixed and the fixes should be included into the software verification competition benchmark via a Merge Request.

Ranged program analysis [1] is a technique to split the analysis of a program into different parts. The idea is split the program's state space, i.e., its execution paths, into separate parts and analyse each part separately, e.g., in parallel. To describe the different parts, ranged program analysis orders the paths and describes a part by a so-called range. A range is characterized by a lower and upper path that are typically described by a test input and describes all paths that are in order between lower and upper bound. The goal of this thesis, is to make use of the ranges when reverifying a program after change. In its simplest form, reverification should reuse the ranges and simply skip range computation. To this end, ranges need to be stored and read if this is not provided so far. Next to this simple approach, a more complicated approach identifies those ranges that contain modified execution paths, e.g., using the idea of difference verification with conditions [2] and restrict reverification of those ranges. An even more sophisticated approach aims to restrict the ranges such that they focus on modified paths, e.g., strip outer non-modified and possibly split ranges. The different approaches for incremental ranged analysis should be implemented in CPAchecker [3]compared against standard ranged program analysis. A master thesis ideally also looks into theoretical soundness aspects of the approach.

Automatic test-generation approaches have different strengths. To achieve better results, e.g., higher branch coverage, distinct test-generation approaches should be combined. One method to combine different approaches is algorithm selection, i.e., a selector chooses from a given set of approaches a most suitable approach for the particular test-case generation task (program). This method has already been successfully applied for software verification, e.g., [1]. The goal of this thesis is to apply algorithm selection to the verification-based test-case generation approaches available in the software analysis framework CPAchecker [2]. To this end, the thesis should first compare the performance of different analyses like Predicate Abstraction, Value Analysis, BMC, and symbolic execution with respect to covered test goals on the software verification competition benchmark [3] (in particular its test tasks). Thereby, it should be analyzed how well the features from [1] are suited to determine the best analysis per test task and study , whether there exist program features that would allow for a better determination. In a second step, the determined selection based on the identified features should be implemented in CPAchecker [2], e.g., as an extension of the SelectionAlgorithm together with an appropriate configuration. Ideally, the realized selection procedure is evaluated on the benchmark of the International Competition on Software Testing.

Automatic test-generation approaches have different strengths. To achieve better results, e.g., higher branch coverage, distinct test-generation approaches should be combined. One method to combine different approaches is the CoVeriTest [1] approach that interleaves different analysis for test-case generation providing each analysis with an individual time limit for each iteration. In this thesis, we want to use the principle of algorithm selection to choose the time limits per task. Algorithm selection has already been successfully applied for software verification, e.g., [2]. Similar to [2], the goal of this thesis is to use program features to define a selector for the time limits. As a starting point, it should be analyzed how well the features from [2] are suited to select the time limits and whether there exist program features that would allow for a better selection. In a second step, the determined selection based on the identified features should be integrated into CoVeriTest, which is implemented in CPAchecker [2]. Ideally, the realized selection procedure is evaluated on the benchmark of the International Competition on Software Testing.

After a program change, the program needs to be reverified. Reverifying the program from scratch can be inefficient and incremental verification techniques try to increase the performance of reverification by reusing information from a previous verification. The goal of this thesis is to propose a solution to use correctness witnesses (in GraphML or in YAML format [1]) to make reverification with k-Induction [2] more efficient. k-Induction already uses correctness witnesses for validation, i.e., reverification of the same instead of a changed program. However, for reverification of a changed program one needs to deal with the changes. Due to the change, the witness information cannot directly be mapped to the program, e.g., because loop locations changed. Therefore, the thesis needs to consider where to map the information from the witness, e.g., one could apply loop invariants to all loops of the function or the closest loop. The developed solution should be implemented in the software analysis framework CPAchecker [3]. In addition, an evaluation should study whether the use of correctness witnesses can improve the efficiency or effectiveness of k-induction. The evaluation may use correctness witnesses constructed by k-Induction or other analyses.

Conditional Model Checking [1] is a technique to split the analysis of a program into several analyses that each analyze parts of the program paths. Thereby, the part an analyzer should explore is encoded into a condition, an automata like format, which accepts all program paths except for the paths that should be analyzed. The goal of this thesis, is to make use of the ranges when reverifying a program after change. The challenge is to ensure that also the modified program paths are analyzed, i.e., are not excluded from analysis. To guarantee this property, existing conditions might need to be updated or new conditions for modified paths that are not covered by the existing conditions must be defined.
In its simplest form, reverification should adapt the set of conditions to include also the modified behavior. Next to this simple approach, a more complicated approach identifies those conditions that contain only non-modified execution paths, e.g., using the idea of difference verification with conditions [2], and excludes them from reverification. An even more sophisticated approach aims to restrict the conditions such that they focus on modified paths, e.g., use a product composition of the condition from difference verification [2] and the original condition. The different approaches for incremental conditional model checking should be implemented in CPAchecker [3] and compared against standard conditional model checking. Also, the soundness of the approach must be shown, i.e., it must be formally proven that all modified paths are verified