Booster: An acceleration-based verification framework for array programs*

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

Research output: Chapter in Book/Report/Conference proceedingConference contribution

11 Citations (Scopus)

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.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings
PublisherSpringer Verlag
Pages18-23
Number of pages6
Volume8837
ISBN (Print)9783319119359
Publication statusPublished - 2014
Event12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014 - Sydney, Australia
Duration: Nov 3 2014Nov 7 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8837
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014
CountryAustralia
CitySydney
Period11/3/1411/7/14

Fingerprint

Interpolants
Safety
Integrate
Scaling
Invariant
Framework
Abstraction
Standards

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Alberti, F., Ghilardi, S., & Sharygina, N. (2014). Booster: An acceleration-based verification framework for array programs*. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings (Vol. 8837, pp. 18-23). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8837). Springer Verlag.

Booster : An acceleration-based verification framework for array programs*. / Alberti, Francesco; Ghilardi, Silvio; Sharygina, Natasha.

Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. Vol. 8837 Springer Verlag, 2014. p. 18-23 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 8837).

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Alberti, F, Ghilardi, S & Sharygina, N 2014, Booster: An acceleration-based verification framework for array programs*. in Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. vol. 8837, Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 8837, Springer Verlag, pp. 18-23, 12th International Symposium on Automated Technology for Verification and Analysis, ATVA 2014, Sydney, Australia, 11/3/14.
Alberti F, Ghilardi S, Sharygina N. Booster: An acceleration-based verification framework for array programs*. In Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. Vol. 8837. Springer Verlag. 2014. p. 18-23. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
Alberti, Francesco ; Ghilardi, Silvio ; Sharygina, Natasha. / Booster : An acceleration-based verification framework for array programs*. Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings. Vol. 8837 Springer Verlag, 2014. pp. 18-23 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@inproceedings{8013a4b2d13a4868b79916ac9185e7b9,
title = "Booster: An acceleration-based verification framework for array programs*",
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.",
author = "Francesco Alberti and Silvio Ghilardi and Natasha Sharygina",
year = "2014",
language = "English",
isbn = "9783319119359",
volume = "8837",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer Verlag",
pages = "18--23",
booktitle = "Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings",

}

TY - GEN

T1 - Booster

T2 - An acceleration-based verification framework for array programs*

AU - Alberti, Francesco

AU - Ghilardi, Silvio

AU - Sharygina, Natasha

PY - 2014

Y1 - 2014

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=84908692460&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84908692460&partnerID=8YFLogxK

M3 - Conference contribution

AN - SCOPUS:84908692460

SN - 9783319119359

VL - 8837

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 18

EP - 23

BT - Automated Technology for Verification and Analysis - 12th International Symposium, ATVA 2014, Proceedings

PB - Springer Verlag

ER -