There are many hard verification problems that are currently only solvable by applying several verifiers that are based on complementing technologies. Conditional model checking (CMC) is a successful solution for cooperation between verification tools. In CMC, the first verifier outputs a condition describing the state space that it successfully verified. The second verifier uses the condition to focus its verification on the unverified state space. To use arbitrary second verifiers, we recently proposed a reducer-based approach. One can use the reducer-based approach to construct a conditional verifier from a reducer and a (non-conditional) verifier: the reducer translates the condition into a residual program that describes the unverified state space and the verifier can be any off-the-shelf verifier (that does not need to understand conditions). Until now, only one reducer was available. But for a systematic investigation of the reducer concept, we need several reducers. To fill this gap, we developed FRed, a Framework for exploring different REDucers. Given an existing reducer, FRed allows us to derive various new reducers, which differ in their trade-off between size and precision of the residual program. For our experiments, we derived seven different reducers. Our evaluation on the largest and most diverse public collection of verification problems shows that we need all seven reducers to solve hard verification tasks that were not solvable before with the considered verifiers.
Reducer-based conditional model checker configurations consists of three components: the condition-generating verifier v1, the reducer r, and the second verifier v2 (the latter two forming the conditional verifier). In our experiments, we use 84 condition model checkers configurations. All either use a predicate analysis or a value analysis for the condition-generating verifier v1. We combine these condition-generating verifiers with 43 different conditional verifiers, each composing a reducer and a second verifier. However, we excluded the two combinations using the same verifier for v1 and v2. For the reducer, we consider seven different fold-reducers: CFA, LH, LHC, LHB, LHBC, NLH, and SEP. For the details, we refer to our paper. These reducers are combined with one of seven verifiers v2. For the second verifiers, we use
The goal of the reducer study is to systematically investigate the effect of different reducers in reducer-based conditional model checking. To this end, we experiment with different reducer-based conditional model checking configurations. For our study, we considered the largest publicly available benchmark collection of C verification tasks. We focused on the 6,907 tasks that consider safety properties (i.e., the program never calls __VERIFIER_error()), which are supported by all verifiers used in the reducer-based conditional model-checking configurations. Additionally, we excluded the easy tasks, i.e., all tasks that any of the conditional model-checking configurations could solve only using one of its verifiers and the tasks for which all reducers fail to generate a residual program (e.g., due to errors, unsupported features like recursion, etc.). To determine the task set for experiments, we performed a task selection experiment. Furthermore, we split the evaluation of reducer-based conditional model-checking configurations into two parts: the initial, condition generating verification, which is incomplete, and the evaluation of the subsequent conditional verifier. Thus, we ensure that all configurations with the same initial verifier use the same input condition for the second, conditional verifier and avoid that the effect of the reducer is tampered by different input conditions. Finally, we separately study the sizes of the residual programs generated by the reducers used in our conditional verifiers.
1) Task Selection
The goal of the task selection experiment is to determine the easy tasks, i.e., tasks that each conditional model-checking configuration could solve using only one of its verifiers. A reducer-based conditional model-checking configurations use two verifiers, a condition-generating verifier v1 and a second verifier v2.
In our task selection experiment, we run the two condition generating verifiers with their time limit of 100 s and verifiers taking part in a conditional verifier for 1000 s (the total time limit of each CMC configuration). The following table shows the raw data (XML and log files) obtained by running all four verifiers. The last row of the table links to the generated HTML and CSV tables, which unite the results of all runs.
| Condition-generating verifiers v1 (100 s) | Verifiers v2 | ||||||||
|---|---|---|---|---|---|---|---|---|---|
| Predicate analysis | Value analysis | CPAseq | ESBMC | k-induction | Predicate analysis | Symbiotic | Value analysis | VeriAbs | All Verifiers |
| Log Files | Log Files | Log Files | Log Files | Log Files | Log Files | Log Files | Log Files | Log Files | HTML Table |
| Result XML | Result XML | Result XML | Result XML | Result XML | Result XML | Result XML | Result XML | Result XML | CSV Table |
2) Condition Generating Verifier
As already explained, we split the evaluation of the conditional model checking configurations into two parts: the evaluation of the initial, condition generating verifier and the evaluation of the conditional verifier. Independent how often an initial, condition generating verifier is used in a conditional model checking configuration, we run the initial condition generating verifier once on each benchmark program. Thus, for each task the conditional verifiers get the same input: program task and condition. The following table shows the results for the condition-generating verifiers used, the predicate analysis and the value analysis.
| Predicate analysis | HTML Table | CSV Table | Log Files | Result XML | Conditions |
| Value analysis | HTML Table | CSV Table | Log Files | Result XML | Conditions |
Note that we internally limited the time of the verifier to 100 s, but we used a larger hard time limit (220 s) to ensure that the conditions are likely written completely. However, as the log files reveal, the internal limit does not work properly when executing some components of the analysis like e.g. the counterexample check. Furthermore, note that due to small deviations in the experiments, some tasks that are close to the time limit of 100 s that could not be solved during the task selection experiment, could be solved in this experiment. We decided to also excluded those tasks from the subsequent evaluation.
3) Conditional Verifiers
Conditional model checker consists a condition-generating model checker followed by a conditional verifier. In the previous section, we presented the experimental data for the condition-generating verifier. Now, we provide the results for the conditional verifiers. Our conditional verifiers are reducer-based, i.e., they compose a reducer r and a second verifier v2. In our experiments, we combine seven fold-reducers (CFA, LH, LHC, LHB, LHBC, NLH, and SEP, for the details see the paper) with six verifiers v2. The following table shows for each condition generating verifier the results for all 21 conditional verifiers, which are applied to pairs of program task and corresponding condition generated by that condition-generating verifier. Each row groups the results of conditional verifiers using the same second verifier and one of the seven fold-reducers. The first two columns of each row describe the fixed verifier components.
| Condition Generating Verifier v1 | Verifier v2 | |||
|---|---|---|---|---|
| Predicate analysis | CPAseq | HTML Table | CSV Table | Log Files |
| Predicate analysis | ESBMC | HTML Table | CSV Table | Log Files |
| Predicate analysis | k-induction | HTML Table | CSV Table | Log Files |
| Predicate analysis | Symbiotic | HTML Table | CSV Table | Log Files |
| Predicate analysis | Value analysis | HTML Table | CSV Table | Log Files |
| Predicate Analysis | VeriAbs | HTML Table | CSV Table | Log Files |
| Value analysis | CPAseq | HTML Table | CSV Table | Log Files |
| Value analysis | ESBMC | HTML Table | CSV Table | Log Files |
| Value analysis | k-induction | HTML Table | CSV Table | Log Files |
| Value analysis | Predicate analysis | HTML Table | CSV Table | Log Files |
| Value analysis | Symbiotic | HTML Table | CSV Table | Log Files |
| Value analysis | VeriAbs | HTML Table | CSV Table | Log Files |
| Result XML for all conditional verifier runs | ||||
To identify the tasks that the ParComp reducer (SEP reducer) cannot solve, but that could be solved with another reducer, you can use the filter rows option in the HTML table.
The easiest way to get to know these tasks is to look at each non-ParComp reducer separately and identify those tasks that the ParComp reducer cannot solve, but the particular non-ParComp reducer can solve.
To this end, first select status correct for the ParComp reducer and press the invert filter button.
Then, chose status correct for the respective non-ParComp reducer and press filter.
Similarly, you may use the filter option to identify that can only be solved with one particular reducer.
We suggest to identify these tasks per reducer.
To this end, choose one reducer and first restrict the tasks to all tasks for which the conditional verifier using this reducer reports a correct result.
Next, use the filter to remove all tasks that conditional verifiers based on other reducers also solved.
To this end, select status correct and press the invert filter button.
4) Residual Program Sizes
To study the difference of the size of residual programs generated by different reducers, we only executed the reducers (without a subsequent, second verifier) and then parsed the program to get the number of locations for the residual program. The following table shows the experimental results for this experiment.
| Verifier v1 | Reducer Execution | |||
|---|---|---|---|---|
| Predicate analysis | HTML Table | CSV Table | Log Files | Result XMLs |
| Value analysis | HTML Table | CSV Table | Log Files | Result XMLs |
The following explanation assumes that there exists a base directory, referenced to with $BASE in the following, to which you want to extract all the data and programs that are necessary to reproduce the results.
The easiest way for the environmental setup is to use our artifact and follow the README instructions. Alternatively, you can perform the following steps.
cd $BASE svn checkout https://svn.sosy-lab.org/software/cpachecker/trunk@32965 CPAchecker
cd $BASE wget https://gitlab.com/sosy-lab/sv-comp/archives-2020/raw/svcomp20/2020/cpa-seq.zip unzip cpa-seq.zip mv CPAchecker-1.9-unix cpa-seq
cd $BASE wget https://gitlab.com/sosy-lab/sv-comp/archives-2020/raw/svcomp20/2020/esbmc.zip unzip esbmc.zip
cd $BASE wget https://gitlab.com/sosy-lab/sv-comp/archives-2020/raw/svcomp20/2020/symbiotic.zip unzip symbiotic.zip
cd $BASE wget https://gitlab.com/sosy-lab/sv-comp/archives-2020/raw/svcomp20/2020/veriabs.zip unzip veriabs.zip mv veriabs/VeriAbs VeriAbs
unzip coverif.zip -d $BASE
cd $BASE git clone https://github.com/sosy-lab/sv-benchmarks.git sv-benchmarks cd sv-benchmarks git checkout svcomp20
unzip bench_defs.zip -d $BASE
In the following, we provide a small tutorial explaining how to use the framework FRed to build and execute reducer-based conditional model-checking configurations.
For our tutorial, we consider the program count_by_1.i from the benchmark programs (folder loop-new).
The tutorial assumes a program written for a 32-bit architecture. To use the approach for 64-bit programs, replace 32 by 64 in the commands.
As in our experiments, we perform the conditional model checking in two steps.
Go to the base directory.
cd $BASE/CPAchecker/Run the condition generating verifier.
scripts/cpa.sh -spec ../sv-benchmarks/c/properties/unreach-call.prp -predicateAnalysis -32 \ -setprop analysis.collectAssumptions=true -setprop counterexample.continueAfterInfeasibleError=false \ -setprop assumptions.automatonFile=AssumptionAutomaton.txt -setprop assumptions.compressAutomaton=true \ -setprop assumptions.export.location=false -setprop assumptions.automatonIgnoreAssumptions=true \ -setprop CompositeCPA.cpas=cpa.location.LocationCPA,cpa.callstack.CallstackCPA,cpa.functionpointer.FunctionPointerCPA,cpa.predicate.PredicateCPA,\ cpa.assumptions.storage.AssumptionStorageCPA,cpa.conditions.global.GlobalConditionsCPA \ -setprop cpa.conditions.global.time.cpu=100s \ ../sv-benchmarks/c/loop-new/count_by_1.i
The condition is stored in $BASE/CPAchecker/output/AssumptionAutomaton.txt.
Alternatively, you can run the condition generator using the value analysis with the following command.
scripts/cpa.sh -spec ../sv-benchmarks/c/properties/unreach-call.prp -valueAnalysis -32 \ -setprop analysis.collectAssumptions=true -setprop counterexample.continueAfterInfeasibleError=false \ -setprop assumptions.automatonFile=AssumptionAutomaton.txt -setprop assumptions.compressAutomaton=true \ -setprop assumptions.export.location=false -setprop assumptions.automatonIgnoreAssumptions=true \ -setpropCompositeCPA.cpas=cpa.location.LocationCPA,cpa.callstack.CallstackCPA,cpa.functionpointer.FunctionPointerCPA,cpa.value.ValueAnalysisCPA, \ cpa.assumptions.storage.AssumptionStorageCPA,cpa.conditions.global.GlobalConditionsCPA -setprop cpa.conditions.global.time.cpu=100s \ ../sv-benchmarks/c/loop-new/count_by_1.i
We implemented a small script to realize the conditional verifier. The script allows to configure the reducer and the second verifier v2 and realizes the sequential execution of reducer and verifier. In the following, we explain the execution of the conditional verifiers.
Go to the base directory.
cd $BASE
To run the conditional verifiers, execute the following command replacing place holders $REDUCER and $VERIFIER as explained below.
conditional_verifiers_fold.sh $REDUCER $VERIFIER \ "CPAchecker/output/AssumptionAutomaton.txt" \ 32 \ sv-benchmarks/c/properties/unreach-call.prp \ sv-benchmarks/c/loop-new/count_by_1.i
Our conditional verifier script supports all seven reducers, we developed. To define the reducer, placeholder $REDUCER must be replaced by one of the following values: cfa, lh, lhc, lhb, lhbc, nlh, sep. The naming of the reducer values reflects correspondence to the actual reducers. To fix the verifier, use the following values for placeholder $VERIFIER: value cpaSeq for CPAseq, esbmc for ESBMC, symbiotic for Symbiotic, veriabs for VeriAbs, kInduction for k-induction, value for value analysis, and predicate for predicate analysis.
For example, if you want to use the NLH reducer together with CPAseq, you need to run the following command.
conditional_verifiers_fold.sh nlh cpaSeq \ "CPAchecker/output/AssumptionAutomaton.txt" \ 32 \ sv-benchmarks/c/properties/unreach-call.prp \ sv-benchmarks/c/loop-new/count_by_1.i
To repeat the task selection experiment, run the following commands.
cd $BASE/CPAchecker benchexec --container ../bench_defs/kinduction.xml benchexec --container ../bench_defs/predicate.xml benchexec --container ../bench_defs/predicate100.xml benchexec --container ../bench_defs/value.xml benchexec --container ../bench_defs/value100.xml cd $BASE/cpa-seq benchexec --container ../bench_defs/cpa-seq.xml cd $BASE/esbmc benchexec --container ../bench_defs/esbmc.xml cd $BASE/symbiotic benchexec --container ../bench_defs/symbiotic.xml cd $BASE/VeriAbs benchexec --container ../bench_defs/veriabs.xml
We split the conditional model checking experiments in two steps: execution of the condition-generation verifier and execution of the conditional verifiers.
Here, we explain how to repeat the experiments for the condition-generation verifier predicate analysis and the condition-generating verifier value analysis..
To rerun the experiments with the condition-generating verifier predicate analysis and create the respective conditions, run the following command.
cd $BASE/CPAchecker benchexec --container ../bench_defs/predicate-cond.xml
To rerun the experiments with the condition-generating verifier value analysis and create the respective conditions, run the following command.
cd $BASE/CPAchecker benchexec --container ../bench_defs/value-cond.xml
To reexecute the experiment analyzing the residual program sizes, run the following commands.
cd $BASE/CPAchecker benchexec --container ../bench_defs/red-pred+prog.xml benchexec --container ../bench_defs/red-val+prog.xml
We split the conditional model checking experiments in two steps: execution of the condition-generation verifier and execution of the conditional verifiers. Here, we explain how to repeat the experiments for the conditional verifiers. Our conditional verifiers consist of the reducer and the second verifier. Our experiment for the conditional verifiers consists of one subexperiment per pair of verifier v1 and v2. Each subexperiment fixes the second verifier v2 and uses the conditions produced by the condition-generating verifier v1. For each subexperiment, all configurations that use the respective second verifier and one of the seven reducers are evaluated.
To execute the resulting four subexperiments run the following commands.
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-pred+cpaseq.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-pred+esbmc.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-pred+kInduction.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-pred+symbiotic.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-pred+value.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-pred+veriabs.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-val+cpaseq.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-val+esbmc.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-val+kInduction.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-val+predicate.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-val+symbiotic.xml
cd $BASE export PYTHONPATH=$PYTHONPATH:. benchexec --container bench_defs/red-val+veriabs.xml
Note that we use the conditions that we generated for the reexecution.
To generate the graph shapes, execute the following commands.
cd $BASE/CPAchecker benchexec --container ../bench_defs/red-pred+pixel.xml benchexec --container ../bench_defs/red-val+pixel.xml