Technical report detail

Decision Procedures for Flat Array Properties

by Francesco Alberti, Silvio Ghilardi, Natasha Sharygina

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.

Technical report 2013/04, October 2013

BibTex entry

@techreport{13decision, author = {Francesco Alberti and Silvio Ghilardi and Natasha Sharygina}, title = {Decision Procedures for Flat Array Properties}, institution = {University of Lugano}, number = {2013/04}, year = 2013, month = oct }