with Refinement Selection
Competition Contribution to SV-COMP'16
This is a special version of CPAchecker . It presents the two concepts sliced path prefixes  and refinement selection  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.
 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.
 D. Beyer, S. Löwe, and P. Wendler. Refinement selection. In Proc. SPIN, LNCS 9232, pages 20–38. Springer, 2015.
 S. Löwe. CPA-RefSel, based on revision 18373 of CPAchecker, branch refinementSelectionForABE, 8th November 2015.
21.01.2016 CPA-RefSel wins the gold medal in the category DeviceDriversLinux64.
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.