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.
Booster : an Acceleration-Based Verification Framework for Array Programs / F. Alberti, S. Ghilardi, N. Sharygina (LECTURE NOTES). - In: Automated technology for verification and analysis : 12th International Symposium, ATVA 2014 Sydney, NSW, Australia, November 3-7, 2014, proceedings / [a cura di] F. Cassez, J.F. Raskin. - Cham : Springer, 2014. - ISBN 9783319119366. - pp. 18-23 (( Intervento presentato al 12. convegno Automated Technology for Verification and Analysis (ATVA) Symposium tenutosi a Sydney nel 2014.
Booster : an Acceleration-Based Verification Framework for Array Programs
S. Ghilardi;
2014
Abstract
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.
| File | Dimensione | Formato | |
|---|---|---|---|
|
ATVA_2014.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
276.53 kB
Formato
Adobe PDF
|
276.53 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
