For some classes of guarded ground assignments for arrays, we show that accelerations (i.e. transitive closures) are definable in the theory of arrays via ∃∗ ∀∗ -first order formulae. We apply this result to model checking of unbounded array programs, where the computation of such accelerations can be used to prevent divergence of reachability analysis. To cope with nested quantifiers introduced by acceleration pre-processing, we use simple instantiation and refinement strategies during backward search analysis. Our new acceleration technique and abstraction/refinement loops are mutually beneficial: experiments conducted with the SMT-based model checker mcmt attest the effectiveness of our approach where acceleration and abstraction/refinement technologies fail if applied alone.

Definability of Accelerated Relations in a Theory of Arrays and its Applications / F. Alberti, S. Ghilardi, N. Sharygina - In: Frontiers of Combining Systems : 9th International Symposium, FroCoS 2013, Nancy, France, September 18-20, 2013, Proceedings / [a cura di] P. Fontaine, C. Ringeissen, R.A. Schmidt. - [s.l] : Springer, 2013 Sep. - ISBN 978-3-642-40884-7. - pp. 23-39 (( Intervento presentato al 9. convegno Frocos tenutosi a Nancy nel 2013 [10.1007/978-3-642-40885-4_3].

Definability of Accelerated Relations in a Theory of Arrays and its Applications

S. Ghilardi
Secondo
;
2013

Abstract

For some classes of guarded ground assignments for arrays, we show that accelerations (i.e. transitive closures) are definable in the theory of arrays via ∃∗ ∀∗ -first order formulae. We apply this result to model checking of unbounded array programs, where the computation of such accelerations can be used to prevent divergence of reachability analysis. To cope with nested quantifiers introduced by acceleration pre-processing, we use simple instantiation and refinement strategies during backward search analysis. Our new acceleration technique and abstraction/refinement loops are mutually beneficial: experiments conducted with the SMT-based model checker mcmt attest the effectiveness of our approach where acceleration and abstraction/refinement technologies fail if applied alone.
array theory ; software model checking
Settore INF/01 - Informatica
set-2013
http://www.springer.com/computer/ai/book/978-3-642-40884-7
Book Part (author)
File in questo prodotto:
Non ci sono file associati a questo prodotto.
Pubblicazioni consigliate

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/2434/224416
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 12
  • ???jsp.display-item.citation.isi??? 11
social impact