Result: Polyhedra to the rescue of array interpolants

Title:
Polyhedra to the rescue of array interpolants
Authors:
Alberti, Francesco, Monniaux, David
Contributors:
Faculty of Informatics [Lugano], Università della Svizzera italiana = University of Italian Switzerland (USI), VERIMAG (VERIMAG - IMAG), Université Joseph Fourier - Grenoble 1 (UJF)-Institut polytechnique de Grenoble - Grenoble Institute of Technology (Grenoble INP)-Institut National Polytechnique de Grenoble (INPG)-Centre National de la Recherche Scientifique (CNRS), ERC STATOR +Swiss National Science Foundation grant no. P1TIP2_152261, European Project: 306595,ERC-2012-StG_20111012,ERC-2012-StG_20111012,STATOR(2013)
Source:
ACM/SIGAPP Symposium On Applied Computing. :1745-1750
Publisher Information:
CCSD; Association for computing machinery, 2015.
Publication Year:
2015
Collection:
collection:UGA
collection:IMAG
collection:CNRS
collection:UNIV-GRENOBLE1
collection:INPG
collection:VERIMAG
collection:TEST-UGA
Subject Terms:
arrays, interpolation, program verification, inductive invariants, ACM: D.: Software, D.2: SOFTWARE ENGINEERING, D.2.4: Software, Program Verification, ACM: F.: Theory of Computation, F.3: LOGICS AND MEANINGS OF PROGRAMS, F.3.1: Specifying and Verifying and Reasoning about Programs, [INFO.INFO-PL]Computer Science [cs], Programming Languages [cs.PL], [INFO.INFO-LO]Computer Science [cs], Logic in Computer Science [cs.LO]
Subject Geographic:
Salamanca, Spain
Original Identifier:
HAL: hal-01178600
Document Type:
Conference conferenceObject<br />Conference papers
Language:
English
Relation:
info:eu-repo/semantics/altIdentifier/doi/10.1145/2695664.2695784; info:eu-repo/grantAgreement//306595/EU/STATic analysis with ORiginal methods/STATOR
DOI:
10.1145/2695664.2695784
Access URL:
https://hal.science/hal-01178600
https://hal.science/hal-01178600v1/document
https://hal.science/hal-01178600v1/file/Monniaux_Alberti_SAC-SVT_2015.pdf
Rights:
info:eu-repo/semantics/OpenAccess
Accession Number:
edshal.hal.01178600v1
Database:
HAL

Further Information

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.