@conference {185, title = {Decision Procedures for Flat Array Properties}, booktitle = {TACAS}, year = {2014}, publisher = {Springer}, organization = {Springer}, address = {Grenoble, France}, abstract = {
We present new decidability results for quantified fragments\ of theories of arrays. Our decision procedures are fully declarative, parametric in the theories of indexes and elements and orthogonal with respect to known results. We also discuss applications to the analysis of\ programs handling arrays.
}, author = {Francesco Alberti and Ghilardi, S. and Natasha Sharygina} }