Implementation of DAR in CPAchecker
This MR implements DAR model checking algorithm (https://link.springer.com/chapter/10.1007/978-3-642-36742-7_22) in CPAchecker. It creates two new classes with main code: DARAlgorithm
, DualInterpolationSequence
Since it mainly uses interpolation, we compared it to other algorithms that use interpolation IMC and ISMC on ReachSafety SV-comp tasks, the results are attached: results.2023-08-31_13-59-31.table.html
DAR shares similar functions with IMC/ISMC, we could either create interface or abstract class for them in the next merge request.
This MR is only for code review. Merging has to be done via SVN.
Edited by Po-Chun Chien