PV2 ⊧ PeSCo: Predicting Sequential Combinations of Verifiersgenerates the best fitting configuration for CPAchecker that fits previous experiences

PeSCo is a tool for predicting a (likely best) sequential combination of verifiers on a given verification task and then running it

Application domain/field

• Machine learning
• Configurations
• Rank prediction
• Performance prediction

Type of tool

Meta-tool, predicts which combination of verifier configurations to use

Expected input

• Program
• Specification(s) to check

Format:

• Program: .c file
• Specification(s): .spc file
• If given default.spc, it will look for labels named ERROR (case insensitive) and assertions in the source code.

Expected output

In the console, or in an interactive HTML report, it reports whether the specification holds (result is TRUE) or not (result is FALSE). If the specification does not hold, a counterexample is also generated. It also generates visualizations of the program (e.g. abstract reachability tree), coverage information, and time statistics.

Internals

PeSCO uses machine learning to learn a ranking of verifiers on verification tasks. This ordering of verifiers is based on the SV-COMP scoring schema. It uses CPAchecker (with different configurations) as base verifiers. It uses MathSAT 5. PeSCo is integrated in CPAchecker.