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. - (2016 Feb).
Counting Constraints in Flat Array Fragments
S. Ghilardi;E. Pagani
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 in questo prodotto:
File | Dimensione | Formato | |
---|---|---|---|
ARXIV_1602.00458v1.pdf
accesso aperto
Tipologia:
Publisher's version/PDF
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.