Polyhedra to the rescue of array interpolants

Francesco Alberti, David Monniaux

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

4 Citations (Scopus)

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 languageEnglish
Title of host publicationProceedings of the ACM Symposium on Applied Computing
PublisherAssociation for Computing Machinery
Pages1745-1750
Number of pages6
Volume13-17-April-2015
ISBN (Print)9781450331968
DOIs
Publication statusPublished - Apr 13 2015
Event30th Annual ACM Symposium on Applied Computing, SAC 2015 - Salamanca, Spain
Duration: Apr 13 2015Apr 17 2015

Other

Other30th Annual ACM Symposium on Applied Computing, SAC 2015
CountrySpain
CitySalamanca
Period4/13/154/17/15

Fingerprint

Interpolation
Costs
Experiments

Keywords

  • Abstract interpretation
  • Arrays
  • Quantified invariants
  • Software model checking

ASJC Scopus subject areas

  • Software

Cite this

Alberti, F., & Monniaux, D. (2015). Polyhedra to the rescue of array interpolants. In Proceedings of the ACM Symposium on Applied Computing (Vol. 13-17-April-2015, pp. 1745-1750). Association for Computing Machinery. https://doi.org/10.1145/2695664.2695784

Polyhedra to the rescue of array interpolants. / Alberti, Francesco; Monniaux, David.

Proceedings of the ACM Symposium on Applied Computing. Vol. 13-17-April-2015 Association for Computing Machinery, 2015. p. 1745-1750.

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

Alberti, F & Monniaux, D 2015, Polyhedra to the rescue of array interpolants. in Proceedings of the ACM Symposium on Applied Computing. vol. 13-17-April-2015, Association for Computing Machinery, pp. 1745-1750, 30th Annual ACM Symposium on Applied Computing, SAC 2015, Salamanca, Spain, 4/13/15. https://doi.org/10.1145/2695664.2695784
Alberti F, Monniaux D. Polyhedra to the rescue of array interpolants. In Proceedings of the ACM Symposium on Applied Computing. Vol. 13-17-April-2015. Association for Computing Machinery. 2015. p. 1745-1750 https://doi.org/10.1145/2695664.2695784
Alberti, Francesco ; Monniaux, David. / Polyhedra to the rescue of array interpolants. Proceedings of the ACM Symposium on Applied Computing. Vol. 13-17-April-2015 Association for Computing Machinery, 2015. pp. 1745-1750
@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 = "4",
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",

}

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

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

ER -