some image logo

HOME

SEARCH

CURRENT ISSUE

REGULAR ISSUES

SPECIAL ISSUES

   Recent

   In Progress

   Archive

   Proposal

SURVEY ARTICLES

AUTHORS

ABOUT

SERVICE

LOGIN

FAQ

SUPPORT

CONTACT

SPECIAL ISSUE:
Selected papers of the "22nd International Conference on Rewriting Techniques and Applications (RTA'11)"



Quantifier-Free Interpolation of a Theory of Arrays

©Roberto Bruttomesso, Università degli Studi di Milano, Department of Computer Science
©Silvio Ghilardi, Università degli Studi di Milano, Department of Computer Science
©Silvio Ranise, Fondazione Bruno Kessler, Trento

Abstract
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.

Publication date: April 27, 2012

Full Text: PDF | PostScript
DOI: 10.2168/LMCS-8(2:4)2012

Hit Counts: 5878

Creative Commons