Skip to content

Draft: Implementation of backward BMC algorithm

Nian-Ze Lee requested to merge BBMC-algorithm-MR-only into trunk

git-svn-id: https://svn.sosy-lab.org/software/cpachecker/branches/BBMC-algorithm-MR-only@44262 4712c6d2-40bb-43ae-aa4b-fec3f1bdfe4c

In this MR, a backward BMC algorithm (and necessary changes to other supportive CPAs) is implemented. It is the second milestone of the Google Summer of Code project by Bas Laarakker.

It depends on !115 for exporting ARGs constructed by a backward analysis.

This MR is only for code review. Merging has to be done via SVN.

Merge request reports