This is a special version of CPAchecker [3]. It presents the two concepts sliced path prefixes [1] and refinement selection [2] in a composite analysis featuring the value and predicate analysis of CPAchecker.

Specifically for the SV-COMP, we made refinement selection applicable together with adjustable-block encoding. Now, we compute abstraction whenever control flow joins, as the analysis performs best with medium-sized blocks, proving that selecting suitable refinements is as important as an appropriate block-encoding strategy.

[1] D. Beyer, S. Löwe, and P. Wendler. Sliced path prefixes: An effective method to enable refinement selection. In Proc. FORTE, LNCS 9039, pages 228–243. Springer, 2015.

[2] D. Beyer, S. Löwe, and P. Wendler. Refinement selection. In Proc. SPIN, LNCS 9232, pages 20–38. Springer, 2015.

[3] S. Löwe. CPARef-Sel, based on revision 18373 of CPAchecker, branch refinementSelectionForABE, 8th November 2015.

21.01.2016 CPA-RefSel wins the gold medal in the category DeviceDriversLinux64.

23.12.2015 Our paper CPA-RefSel: CPAchecker with Refinement Selection has been accepted for presentation at TACAS 2016.

16.11.2015 With revision 18453 refinement selection for ABE has been integrated into the trunk version of CPAchecker. As such, inter- and intra-refinement selection for both the value and the predicate analysis is available for experimenting and enhancements.