@inproceedings{AM15,
title = {Polyhedra to the rescue of array interpolants },
author = {Alberti, Francesco and Monniaux, David},
year = {2015},
booktitle = {ACM Symposium on Applied Computing, software verification and testing track},
eprint = {hal-01178600},
pages = {1745--1750},
publisher = {ACM},
team = {PACSS},
category = {intc},
eprinttype = {HAL},
abstract = {We propose a new approach to the automated verification of the correctness of programs handling arrays. An abstract interpreter supplies auxiliary numeric invariants to an interpolation-based refinement procedure suited to array programs. Experiments show that this combination approach, implemented in an enhanced version of the Booster software model-checker, performs better than the pure interpolationbased approach, at no additional cost.},
}
