key: cord-0048657-0b76fpwm
authors: Jakobs, Marie-Christine
title: CoVeriTest with Dynamic Partitioning of the Iteration Time Limit (Competition Contribution)
date: 2020-03-13
journal: Fundamental Approaches to Software Engineering
DOI: 10.1007/978-3-030-45234-6_30
sha: 4532cb3ebac741271e607b4f2de9dc7c8a4ebedf
doc_id: 48657
cord_uid: 0b76fpwm

Our CoVeriTest submission, which is implemented in the analysis framework CPAchecker, uses verification techniques for automatic test-case generation. To this end, it checks the reachability of every test goal and generates one test case per reachable goal. Instead of checking the reachability of every test goal individually, which is too expensive, CoVeriTest considers all test goals at once and removes already covered goals from future reachability queries. To deal with the diverse set of Test-Comp tasks, CoVeriTest uses a hybrid approach that interleaves value and predicate analysis. In contrast to Test-Comp’19, the time limit per iteration is no longer fixed for an analysis. Instead, we fix the iteration time limit and split it dynamically among the analyses, rewarding analyses that previously covered more test goals per time unit.

Test-case generation approaches have different strengths and weaknesses. To deal with the diverse Test-Comp benchmark, we therefore use an hybrid approach. More concrete, our Test-Comp'20 submission CoVeriTest combines different verification approaches using the idea of cooperative, verifier-based testing [6] . Figure 1 shows the workflow of our CoVeriTest submission. Like in Test-Comp'19, CoVeriTest iteratively combines a value analysis [5] , which only tracks the explicit values of those variables stored in its precision, and a predicate analysis, which applies adjustable block encoding [4] and abstracts at loop heads only. Both analyses use counterexample-guided abstraction refinement [8] To better adjust to the program, we redistribute the iteration time limit among the analyses after each iteration round. Initially, we grant the value analysis 20 s and the predicate analysis 80 s. Thereafter, we use the normalized progresses p V and p P reported by the analyses to compute the new time limits. The normalized progress is the number of test goals covered by the analysis in the round divided by the total number of test goals. If no analysis made progress (p V ≤ 0 and p P ≤ 0), we will reuse the time limits from the current round. Otherwise, we adjust the limits according to Eq. 1 (i ∈ {V, P }). Each analysis gets at least 10 s to avoid to turn it off. The remaining 80 s of the iteration limit are redistributed according to the relative contribution of each analysis. The relative contribution of an analysis is its progress per time limit related to the sum of the progresses per time limit.

The main differences to HybridTiger [11] , which also applies cooperative, verifierbased testing, are that HybridTiger uses multi-goal partitioning [10] and that HybridTiger uses fixed time limits 120 s and 720 s for value and predicate analysis.

CoVeriTest is implemented within the Java-based software-analysis framework CPAchecker [3] , which uses the Eclipse CDT parser 2 and integrates different SMT solvers via the JavaSMT [9] interface. For Test-Comp'20, we rely on CPAchecker's default SMT solver MathSAT5 [7] .

CPAchecker's core is the configurable program analysis framework [2] , which defines the basis for the verification approaches. The framework consists of two parts: configurable program analyses (CPAs) and the CPA algorithm. CPAs like the value and predicate analysis used by CoVeriTest describe program analyses. Therefore, they define the abstract domain and the analysis operators. The CPA algorithm performs the reachability analysis for a given CPA and program.

To integrate further verification techniques, the CPA framework is enhanced with algorithms like counterexample-guided abstraction refinement [8] , the circular algorithm, which performs a continuous iteration over a set of analyses, or the test-case generation algorithm. To produce test cases, the test-case generation algorithm wraps and runs another analysis, generates test cases from counterexamples [1] returned by the wrapped analysis, updates the analysis specification (i.e., removes covered goals), and thereafter continues the wrapped analysis.

CoVeriTest won the third place in the category Cover-Branches and in contrast to Test-Comp'19, became better than KLEE in this category.

The major change of CoVeriTest from Test-Comp'19 to Test-Comp'20 is the dynamic adjustment of the iteration time limits. Thus, many strength and weaknesses are still the same as in Test-Comp'19. CoVeriTest's iterative combination of predicate and value analysis helped to adapt to the diverse set of Test-Comp tasks and its direct search of the test goals lead to few test cases. Also, CoVeriTest has still problems with tasks that contain large arrays because these are not supported by the underlying analyses. Furthermore, CoVeriTest has problems with the new subcategory BusyBox-Memsafety and fails to parse the programs in the new subcategory SQLite-MemSafety. Now, let us discuss the effect of the adjustment of the time limits. For the time limit adjustment, we use the progress of the analyses measured in number of covered goals. Since there only exists one (reachable) test goal per task in the Cover-Error category, either both analyses make no progress in an iteration (p V ≤ 0 and p P ≤ 0) or one analysis covered the goal and CoVeriTest stops. Thus, the time limit adjustment has no effect on the Cover-Error category.

Next, let us consider the Cover-Branches category. Our own comparison of the CoVeriTest submissions for Test-Comp'19 and Test-Comp'20 revealed that the time limit adjustment mainly affects tasks of the ECA subcategory. In total, the coverage value for 320 tasks decreased and the coverage value for 591 tasks increased. Moreover, the increase is typically significantly larger than the decrease (on average 6.3 percent points increase compared to 1.5 percent points decrease). Furthermore, most of the tasks with a difference in the coverage value belong to the ECA subcategory. Therefore, the time limit adjustment pays off. Nevertheless, CoVeriTest could still perform better on the ECA subcategory. We believe that one problem in the ECA subcategory are redundant test goals, which lead to the same or similar test case generated multiple times and, thus, a waste of time.

CoVeriTest is distributed as part of CPAchecker 3 , which requires a Java 8 runtime environment. Our Test-Comp'20 submission, with which we participated in all categories, uses CPAchecker in revision 32236. After the environmental setup, one can run CoVeriTest on program program.i with the following command. The file property.prp is a placeholder for the test specification, either coverage-error-call.prp or coverage-branches.prp. scripts/cpa.sh -testcomp20 -benchmark -heap 10000m -spec property.prp program.i

The command above assumes that program.i runs in a 32-bit environment.

When requiring a 64-bit environment, one needs to add the parameter -64 to the above command. Moreover, if the machine has not enough RAM to handle the specified Java heap memory, one can decrease the value passed with -heap. The test suite generated during the execution of CoVeriTest is written to the directory test-suite, which is a subdirectory within the output directory of CPAchecker. As defined by the Test-Comp rules, the test suite contains a metadata file and test-case files adhering to the required XML format.

CoVeriTest is a component of the open-source project CPAchecker 3 , which is hosted by Dirk Beyer's group at LMU Munich under Apache 2.0. Currently, also members of the Institute for System Programming of the Russian Academy of Sciences, Masaryk University, and Technical University of Darmstadt contribute to CPAchecker. We would like to thank all contributors.

Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.

The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.

Generating tests from counterexamples

Configurable software verification: Concretizing the convergence of model checking and program analysis

CPAchecker: A tool for configurable software verification

Predicate abstraction with adjustableblock encoding

Explicit-state software model checking based on CEGAR and interpolation

CoVeriTest: Cooperative verifier-based testing

The MathSAT5 SMT solver

Counterexample-guided abstraction refinement for symbolic model checking

JavaSMT: A unified interface for SMT solvers in Java

Configurable test-goal set partitioning for multi-goal test-suite generation

HybridTiger: Hybrid model checking and domination-based partitioning for efficient multi-goal test-suite generation (competition contribution)