This paper presents an acceleration-based combination framework for checking the satisfiability of classes of quantified formulae of the theory of arrays. We identify sufficient conditions for which an 'acceleratability' result can be used as a black-box module inside such satisfiability procedures. Besides establishing new decidability results and relating them to results from recent literature, we discuss the application of our combination framework to the problem of checking the safety of imperative programs with arrays.
A new Acceleration-based Combination Framework for Array Properties / F. Alberti, S. Ghilardi, N. Sharygina (LECTURE NOTES IN COMPUTER SCIENCE). - In: Frontiers of Combining Systems / [a cura di] C. Lutz, S. Ranise. - [s.l] : Springer, 2015. - ISBN 9783319242453. - pp. 169-185 (( Intervento presentato al 10. convegno International Symposium on Frontiers of Combining Systems (FroCoS) tenutosi a Wroclaw nel 2015 [10.1007/978-3-319-24246-0_11].
A new Acceleration-based Combination Framework for Array Properties
S. GhilardiSecondo
;
2015
Abstract
This paper presents an acceleration-based combination framework for checking the satisfiability of classes of quantified formulae of the theory of arrays. We identify sufficient conditions for which an 'acceleratability' result can be used as a black-box module inside such satisfiability procedures. Besides establishing new decidability results and relating them to results from recent literature, we discuss the application of our combination framework to the problem of checking the safety of imperative programs with arrays.
| File | Dimensione | Formato | |
|---|---|---|---|
|
main.pdf
accesso riservato
Tipologia:
Post-print, accepted manuscript ecc. (versione accettata dall'editore)
Dimensione
358.52 kB
Formato
Adobe PDF
|
358.52 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.
