We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are fully declarative, para- metric in the theories of indexes and elements and orthogonal with re- spect to known results. We also discuss applications to the analysis of programs handling arrays.
Decision Procedures for Flat Array Properties / F. Alberti, S. Ghilardi, N. Sharygina - In: Tools and Algorithms for the Construction and Analysis of Systems / [a cura di] E. Ábrahám, K. Havelund. - [s.l] : Springer, 2014 Apr. - ISBN 978-3-642-54861-1. - pp. 15-30 (( Intervento presentato al 20. convegno TACAS 2014 tenutosi a Grenoble nel 2014 [10.1007/978-3-642-54862-8_2].
Decision Procedures for Flat Array Properties
S. Ghilardi;
2014
Abstract
We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are fully declarative, para- metric in the theories of indexes and elements and orthogonal with re- spect to known results. We also discuss applications to the analysis of programs handling arrays.
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
