Slicing Abstraction using Path Formulas
|Title||Slicing Abstraction using Path Formulas|
|Publication Type||Technical Report|
|Authors||E. Ermis, J. Hoenicke, A. Podelski, and M. Schäf|
|Year of Publication||2011|
We present a new interpolation based abstraction refinement algorithm for software model-checking. The refinement step uses interpolants computed from an error path to split the abstract states on this path. It incorporates the ideas of slicing abstraction and large block encoding. We run our model-checker on several benchmarks and show empirically that the presented algorithm terminates more often with a result than existing model checking techniques.