Abstraction and Acceleration in SMT-based Model-Checking for Array Programs

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Abstraction (in its various forms) is a powerful established technique in model-checking; still, when unbounded data-structures are concerned, it cannot always cope with divergence…