Polyhedra to the rescue of array interpolants

Francesco Alberti; David Monniaux

doi:10.1145/2695664.2695784

Polyhedra to the rescue of array interpolants

Francesco Alberti, David Monniaux

IRCCS Ospedale San Raffaele

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

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 interpolation-based approach, at no additional cost. Copyright is held by the owner/author(s).

Original language	English
Title of host publication	Proceedings of the ACM Symposium on Applied Computing
Publisher	Association for Computing Machinery
Pages	1745-1750
Number of pages	6
Volume	13-17-April-2015
ISBN (Print)	9781450331968
DOIs	https://doi.org/10.1145/2695664.2695784
Publication status	Published - Apr 13 2015
Event	30th Annual ACM Symposium on Applied Computing, SAC 2015 - Salamanca, Spain Duration: Apr 13 2015 → Apr 17 2015

Other

Other	30th Annual ACM Symposium on Applied Computing, SAC 2015
Country/Territory	Spain
City	Salamanca
Period	4/13/15 → 4/17/15

Keywords

Abstract interpretation
Arrays
Quantified invariants
Software model checking

ASJC Scopus subject areas

Software

Access to Document

10.1145/2695664.2695784

Cite this

@inproceedings{4ccc34a5d65d43cc8eac57994e20e853,

title = "Polyhedra to the rescue of array interpolants",

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 interpolation-based approach, at no additional cost. Copyright is held by the owner/author(s).",

keywords = "Abstract interpretation, Arrays, Quantified invariants, Software model checking",

author = "Francesco Alberti and David Monniaux",

year = "2015",

month = apr,

day = "13",

doi = "10.1145/2695664.2695784",

language = "English",

isbn = "9781450331968",

volume = "13-17-April-2015",

pages = "1745--1750",

booktitle = "Proceedings of the ACM Symposium on Applied Computing",

publisher = "Association for Computing Machinery",

note = "30th Annual ACM Symposium on Applied Computing, SAC 2015 ; Conference date: 13-04-2015 Through 17-04-2015",

}

TY - GEN

T1 - Polyhedra to the rescue of array interpolants

AU - Alberti, Francesco

AU - Monniaux, David

PY - 2015/4/13

Y1 - 2015/4/13

N2 - 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 interpolation-based approach, at no additional cost. Copyright is held by the owner/author(s).

AB - 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 interpolation-based approach, at no additional cost. Copyright is held by the owner/author(s).

KW - Abstract interpretation

KW - Arrays

KW - Quantified invariants

KW - Software model checking

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

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

U2 - 10.1145/2695664.2695784

DO - 10.1145/2695664.2695784

M3 - Conference contribution

AN - SCOPUS:84955444328

SN - 9781450331968

VL - 13-17-April-2015

SP - 1745

EP - 1750

BT - Proceedings of the ACM Symposium on Applied Computing

PB - Association for Computing Machinery

T2 - 30th Annual ACM Symposium on Applied Computing, SAC 2015

Y2 - 13 April 2015 through 17 April 2015

ER -

Polyhedra to the rescue of array interpolants

Abstract

Other

Keywords

ASJC Scopus subject areas

Access to Document

Other files and links

Fingerprint

Cite this