Adjustments for modular CEGAR

This MR contains configurations and different adjustments for modular CEGAR, a decomposition of counterexample-guided abstraction refinement in three stateless, independent components "abstract-model explorer", "feasibility checker" and "precision refiner". As exchange formats, CPAchecker's predmap.txt and the GraphML witness formats can be used.

On example for the classic predicate abstraction with predicate refinement through CEGAR, with predmap.txt to exchange predicates and violation witness graphml for counterexamples:

graph TD
  pred[Predicate Analysis] -- violation witness<br /> --> check
  check[CEX check] -- violation witness --> refiner
  refiner[refiner] -- predmap.txt --> joiner
  joiner{Joiner} -- joined predmap.txt --> pred
  joiner -- joined predmap.txt --> joiner

I'll add open to-dos in a minute.

Edited by Thomas Lemberger

Merge request reports

Loading