We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures (’acceleratio’) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.
Decision procedures for flat array properties / F. Alberti, S. Ghilardi, N. Sharygina. - In: JOURNAL OF AUTOMATED REASONING. - ISSN 0168-7433. - 54:4(2015 Apr), pp. 327-352. [10.1007/s10817-015-9323-7]
Decision procedures for flat array properties
S. GhilardiSecondo
;
2015
Abstract
We present new decidability results for quantified fragments of theories of arrays. Our decision procedures are parametric in the theories of indexes and elements and orthogonal with respect to known results. We show that transitive closures (’acceleratio’) of relation expressing certain array updates produce formulas inside our fragment; this observation will be used to identify a class of programs handling arrays having decidable reachability problem.
| File | Dimensione | Formato | |
|---|---|---|---|
|
art%3A10.1007%2Fs10817-015-9323-7.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
626.65 kB
Formato
Adobe PDF
|
626.65 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
