Booster : an Acceleration-Based Verification Framework for Array Programs

We present Booster, a new framework developed for verifiying programs handling arrays. Booster integrates new acceleration features with standard verification techniques, like Lazy Abstraction with Interpolants (extended to arrays). The new acceleration features are the key for scaling-up in the verification of programs with arrays, allowing Booster to efficiently generate required quantified safe inductive invariants attesting the safety of the input code