Decision Procedures for Flat Array Properties

TitleDecision Procedures for Flat Array Properties
Publication TypeConference Paper
Year of Publication2014
AuthorsAlberti, Francesco, Ghilardi S., and Sharygina Natasha
Conference NameTACAS
Conference LocationGrenoble, France
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.
Full Text