Slicing Abstraction using Path Formulas

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.