Skip to content

Draft: a new sequential composition for SV-COMP '23

Nian-Ze Lee requested to merge svcomp23-config-search into trunk

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/svcomp23-config-search@42203 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c

This MR proposes a new sequential composition for SV-COMP '23. Compared to the old one, it introduces:

  • Distinguishing between loop-free, single-loop, and multiple-loop programs,
  • Using a new analysis (interpolation-based model checking, IMC) for single-loop programs,
  • Separating k-induction and data-flow analysis (i.e., k-induction without auxiliary invariants), and
  • Using the data-flow invariant generator as a standalone analysis.

Merge request reports