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

Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

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

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
Country/TerritoryAustralia
CitySydney
Period11/3/1411/7/14

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Fingerprint

Dive into the research topics of 'Booster: An acceleration-based verification framework for array programs*'. Together they form a unique fingerprint.

Cite this