Decision Procedures for Flat Array Properties
Authors: Francesco Alberti, Silvio Ghilardi and Natasha Sharygina
Paper Information
| Title: | Decision Procedures for Flat Array Properties |
| Authors: | Francesco Alberti, Silvio Ghilardi and Natasha Sharygina |
| Proceedings: | SMT 2014 Proceedings |
| Editors: | Philipp Ruemmer and Christoph M. Wintersteiger |
| Keywords: | Decision procedures, Theory of arrays, Quantifiers, Array programs |
| Abstract: | 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. |
| Pages: | 1 |
| Talk: | Jul 17 15:00 |
| Paper: |  |