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 frag- ments of arithmetic over indexes in applications, especially those related to software verification. In this paper, we propose a quantifier-free in-terpolation solver for the variant of arrays considered in previous work when combined with integer difference logic over indexes.
A combination of rewriting and constraint solving for the quantifier-free interpolation of arrays with integer difference constraints / R. Bruttomesso, S. Ghilardi, S. Ranise (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Frontiers of combining systems : 8th international symposium, FroCoS 2011 Saarbrücken, Germany, october 5-7, 2011 : proceedings / [a cura di] C. Tinelli, V. Sofronie-Stokkermans. - Berlin : Springer, 2011. - ISBN 978-3-642-24363-9. - pp. 103-118 (( Intervento presentato al 8th. convegno International Symposium on Frontiers of Combining Systems tenutosi a Saarbruecken, Germany 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
R. BruttomessoPrimo
;S. GhilardiSecondo
;
2011
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 frag- ments of arithmetic over indexes in applications, especially those related to software verification. In this paper, we propose a quantifier-free in-terpolation solver for the variant of arrays considered in previous work when combined with integer difference logic over indexes.File | Dimensione | Formato | |
---|---|---|---|
2011_Book_FrontiersOfCombiningSystems-pages-1-4,111-126.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
566.62 kB
Formato
Adobe PDF
|
566.62 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.