DROPS

Document

DOI: 10.4230/LIPIcs.RTA.2011.171

Rewriting-based Quantifier-free Interpolation for a Theory of Arrays

Authors: Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

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, with a minor extension to the theory of arrays, it is possible to obtain quantifier-free interpolants. We prove this by designing an interpolating procedure, based on solving equations between array updates. 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 theory of arrays.

Cite as

Roberto Bruttomesso, Silvio Ghilardi, and Silvio Ranise. Rewriting-based Quantifier-free Interpolation for a Theory of Arrays. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 171-186, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{bruttomesso_et_al:LIPIcs.RTA.2011.171,
  author =	{Bruttomesso, Roberto and Ghilardi, Silvio and Ranise, Silvio},
  title =	{{Rewriting-based Quantifier-free Interpolation for a Theory of Arrays}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{171--186},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9},
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.171},
  URN =		{urn:nbn:de:0030-drops-31155},
  doi =		{10.4230/LIPIcs.RTA.2011.171},
  annote =	{Keywords: rewriting, interpolation, arrays, model-checking}
}

Search Results

Documents authored by Bruttomesso, Roberto

Rewriting-based Quantifier-free Interpolation for a Theory of Arrays

Abstract

Cite as

Thanks for your feedback!

Could not send message