We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We establish decidability and complexity results for such a fragment and we implement our algorithms. The experiments run in discharging proof obligations coming from invariant checking and bounded model-checking benchmarks show the practical feasibility of our decision procedure.
Counting constraints in flat array fragments / F. Alberti, S. Ghilardi, E. Pagani (LECTURE NOTES IN COMPUTER SCIENCE). - In: Automated Reasoning / [a cura di] N. Olivetti, A. Tiwari. - [s.l] : Springer Verlag, 2016 Jun. - ISBN 9783319402284. - pp. 65-81 (( Intervento presentato al 8. convegno International Joint Conference on Automated Reasoning tenutosi a Coimbra nel 2016 [10.1007/978-3-319-40229-1_6].
Counting constraints in flat array fragments
S. Ghilardi
;E. PaganiUltimo
2016
Abstract
We identify a fragment of Presburger arithmetic enriched with free function symbols and cardinality constraints for interpreted sets, which is amenable to automated analysis. We establish decidability and complexity results for such a fragment and we implement our algorithms. The experiments run in discharging proof obligations coming from invariant checking and bounded model-checking benchmarks show the practical feasibility of our decision procedure.
| File | Dimensione | Formato | |
|---|---|---|---|
|
IJCAR2016_PRINTED.pdf
accesso riservato
Descrizione: Articolo completo
Tipologia:
Publisher's version/PDF
Dimensione
316.24 kB
Formato
Adobe PDF
|
316.24 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
|
735915.pdf
accesso aperto
Tipologia:
Pre-print (manoscritto inviato all'editore)
Dimensione
261.32 kB
Formato
Adobe PDF
|
261.32 kB | Adobe PDF | Visualizza/Apri |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
