Roberto Bruttomesso ; Silvio Ghilardi ; Silvio Ranise - Quantifier-Free Interpolation of a Theory of Arrays

lmcs:934 - Logical Methods in Computer Science, April 27, 2012, Volume 8, Issue 2 - https://doi.org/10.2168/LMCS-8(2:4)2012
Quantifier-Free Interpolation of a Theory of ArraysArticle

Authors: Roberto Bruttomesso ; Silvio Ghilardi ; Silvio Ranise

    The use of interpolants in model checking is becoming an enabling technology to allow fast and robust verification of hardware and software. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier- free interpolants in general. In this paper, we show that it is possible to obtain quantifier-free interpolants for a Skolemized version of the extensional theory of arrays. We prove this in two ways: (1) non-constructively, by using the model theoretic notion of amalgamation, which is known to be equivalent to admit quantifier-free interpolation for universal theories; and (2) constructively, by designing an interpolating procedure, based on solving equations between array updates. (Interestingly, rewriting techniques are used in the key steps of the solver and its proof of correctness.) To the best of our knowledge, this is the first successful attempt of computing quantifier- free interpolants for a variant of the theory of arrays with extensionality.


    Volume: Volume 8, Issue 2
    Published on: April 27, 2012
    Imported on: October 26, 2011
    Keywords: Computer Science - Logic in Computer Science,F.4.1, F.3.1
    Funding:
      Source : OpenAIRE Graph
    • Automated Validation of Trust and Security of Service-oriented Architectures; Funder: European Commission; Code: 216471

    20 Documents citing this article

    Consultation statistics

    This page has been seen 1072 times.
    This article's PDF has been downloaded 590 times.