Polyhedra to the rescue of array interpolants

Francesco Alberti, David Monniaux

Research output: Chapter in Book/Report/Conference proceedingConference 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 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

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