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. GhilardiSecondo
;
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.Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.