The use of interpolants in model checking is progressively gaining importance. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. To overcome this problem, we have recently proposed a quantifier-free interpolation solver for a natural variant of the theory of arrays. However, arrays are usually combined with fragments of arithmetic over indexes in applications, especially those related to software verification. In this paper, we propose a quantifier-free interpolation solver for the variant of arrays considered in previous work when combined with integer difference logic over indexes. © 2011 Springer-Verlag.

A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints / Bruttomesso, R.; Ghilardi, S.; Ranise, S.. - 6989:(2011), pp. 103-118. (Intervento presentato al convegno 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011 tenutosi a Saarbrucken, deu nel 2011) [10.1007/978-3-642-24364-6_8].

A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints

Ranise S.
2011-01-01

Abstract

The use of interpolants in model checking is progressively gaining importance. The application of encodings based on the theory of arrays, however, is limited by the impossibility of deriving quantifier-free interpolants in general. To overcome this problem, we have recently proposed a quantifier-free interpolation solver for a natural variant of the theory of arrays. However, arrays are usually combined with fragments of arithmetic over indexes in applications, especially those related to software verification. In this paper, we propose a quantifier-free interpolation solver for the variant of arrays considered in previous work when combined with integer difference logic over indexes. © 2011 Springer-Verlag.
2011
Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Germany
Springer Verlag
978-3-642-24363-9
978-3-642-24364-6
Bruttomesso, R.; Ghilardi, S.; Ranise, S.
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints / Bruttomesso, R.; Ghilardi, S.; Ranise, S.. - 6989:(2011), pp. 103-118. (Intervento presentato al convegno 8th International Symposium on Frontiers of Combining Systems, FroCoS 2011 tenutosi a Saarbrucken, deu nel 2011) [10.1007/978-3-642-24364-6_8].
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11572/333330
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo

Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 4
  • ???jsp.display-item.citation.isi??? ND
social impact