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

摘要

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 preprocessing, 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.