Skip to content

Implementation of DAR in CPAchecker

Marek Jankola requested to merge dual-approximate-reachability into trunk

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

Merge request reports