Counting Constraints in Flat Array Fragments
Logic in Computer Science
2016-02-02 v1
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.
Cite
@article{arxiv.1602.00458,
title = {Counting Constraints in Flat Array Fragments},
author = {Francesco Alberti and Silvio Ghilardi and Elena Pagani},
journal= {arXiv preprint arXiv:1602.00458},
year = {2016}
}