1 Verification Approach
ReachSafety
. However, the analysis sequence is often predefined and fixed. In other words, a problem instance might pass through a sequence of unsuccessful verification configurations until it is processed by the right technique or exceeds a time limit.2 Software Architecture
Planning
step in the restart
algorithm employed in the verification framework CPAchecker [3]. The restart
algorithm [10] is used in a sequential combination of verifiers to let the next verifier start on already computed (partial) results of previous verifiers, in particular when the previous verifier could not solve the verification problem. However, instead of executing a fixed list of verification techniques, our algorithm plans an execution order dependent on the verification task to be solved. Our approach consists of the following steps.-
Training. To train our rank predictor, we employ rankings obtained by executing 5 CPAchecker configurations on the verification tasks of SV-COMP 2018. Similar to CPA-Seq [10] from 2018, we use Value Analysis [5], Value Analysis + CEGAR [5], Predicate Analysis [4], k-Induction [1] and Bounded Model Checking [6]. In addition, we introduced and carried out training with a special
UNKNOWN
configuration. This extension will allow our prediction procedure to cut off an analysis when it will most probably fail. -
Planning. As can be seen in Fig. 1, we utilize the preprocessor and control flow automaton (CFA) construction implemented in CPAchecker. Instead of passing the CFA directly to an analysis, we first query our rank prediction process. The prediction process starts by building an intermediate graph representation. This is followed by a feature extraction and the final ranking procedure (details in [7]). If a prediction is not achievable in a certain time frame, we fall back to the standard CPA-Seq.
-
Execution. After planning a sequential composition, we can apply the analyses in the given order. If an analysis fails or exceeds its time limit, we switch to the next configuration. On reaching the
UNKNOWN
configuration, we exit the verification sequence. Instead of leaving the overall process, specialized techniques will be applied in the following situations: For recursive programs we facilitate Block Abstraction Memoization (BAM) [8, 13] and Binary Decision Diagrams (BDD) [2] are used for concurrent programs. Witnesses are written as generated by the verifiers.
3 Strengths and Weaknesses
4 Tool Setup and Configuration
b8d6131
for the competition. To compile the tool, ant
should be executed on the checkout folder. After this step, our tool requires Java 8 and MathSAT 5 as external tools. To verify a test program, CPAchecker is executed with the following command line: For programs expecting a 64 Bit model, add the parameter
. PeSCo participates in category ReachSafety
, Falsification
and Overall
. The corresponding specification can be found in the checkout folder under
config/specification/sv-comp-reachability.spc
.