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.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
If we want to emphasize the way the basic formula \(\beta \) is built up, following the above conventions, we may write it as \(\beta (x, \underline{y},\mathbf{a} (x), \mathbf{a} (\underline{y}))\); here, supposing that \(\mathbf{a} \) is \(a_1, \dots , a_s\), since x is a singleton, the tuple \(\mathbf{a} (x)\) is \(a_1(x), \dots , a_s(x)\).
- 2.
By the quantifier-elimination result for Presburger arithmetic, it is well-known that arithmetic formulæ are equivalent to quantifier-free ones. The same is true for basic formulæ because they are obtained from arithmetic formulae by substitutions without capture.
- 3.
These conjuncts (varying \(\sigma \in \varSigma \)) are needed in (11) to ensure that the assignments we are using can coexist in a model.
- 4.
ArCa stands for Array with Cardinalities.
References
Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments (2016). CoRR, abs/1602.00458
Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 15–30. Springer, Heidelberg (2014)
Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: Proceedings of PODC, pp. 244–253 (2007)
Bjørner, N., von Gleissenthall, K., Rybalchenko, A.: Synthesizing cardinality invariants for parameterized systems (2015). https://www7.in.tum.de/~gleissen/papers/sharpie.pdf
Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. Distrib. Comput. 22, 49–71 (2009)
Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43–112. Academic Press, New York (1968)
Drăgoi, C., Henzinger, T.A., Veith, H., Widder, J., Zufferey, D.: A logic-based framework for verifying consensus algorithms. In: McMillan, K.L., Rival, X. (eds.) VMCAI 2014. LNCS, vol. 8318, pp. 161–181. Springer, Heidelberg (2014)
Dragoi, C., Henzinger, T.A., Zufferey, D.: The need for language support for fault-tolerant distributed systems. In: Proceedings of SNAPL (2015)
Eisenbrand, F., Shmonin, G.: Carathéodory bounds for integer cones. Oper. Res. Lett. 34(5), 564–568 (2006)
Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi ^1_1\) complete. J. Symbol. Logic 56(2), 637–642 (1991)
John, A., Konnov, I., Schmid, U., Veith, H., Widder, J.: Parameterized model checking of fault-tolerant distributed algorithms by abstraction. In: Proceedings of FMCAD, pp. 201–209, August 2013
Konnov, I., Veith, H., Widder, J.: On the completeness of bounded model checking for threshold-based distributed algorithms: reachability. In: Baldan, P., Gorla, D. (eds.) CONCUR 2014. LNCS, vol. 8704, pp. 125–140. Springer, Heidelberg (2014)
Konnov, I., Veith, H., Widder, J.: SMT and POR beat counter abstraction: parameterized model checking of threshold-based distributed algorithms. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 85–102. Springer, Heidelberg (2015)
Kuncak, V., Nguyen, H.H., Rinard, M.: An algorithm for deciding BAPA: boolean algebra with Presburger arithmetic. In: Nieuwenhuis, R. (ed.) CADE 2005. LNCS (LNAI), vol. 3632, pp. 260–277. Springer, Heidelberg (2005)
Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding boolean algebra with Presburger arithmetic. J. Autom. Reasoning 36(3), 213–239 (2006)
Kuncak, V., Rinard, M.: Towards efficient satisfiability checking for boolean algebra with Presburger arithmetic. In: Pfenning, F. (ed.) CADE 2007. LNCS (LNAI), vol. 4603, pp. 215–230. Springer, Heidelberg (2007)
Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of ISCA, p. 348 (1984)
Piskac, R., Kuncak, V.: Decision procedures for multisets with cardinality constraints. In: Logozzo, F., Peled, D.A., Zuck, L.D. (eds.) VMCAI 2008. LNCS, vol. 4905, pp. 218–232. Springer, Heidelberg (2008)
Schweikhart, N.: Arithmetic, first-order logic, and counting quantifiers. ACM TOCL 6, 1–35 (2004)
Solihin, Y.: Fundamentals of Parallel Computer Architecture Multichip and Multicore Systems. Solihin Publishing & Consulting LLC (2008)
Srikanth, T.K., Toueg, S.: Optimal clock synchronization. J. ACM 34(3), 626–645 (1987)
Srikanth, T.K., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib. Comput. 2(2), 80–94 (1987)
Yessenov, K., Piskac, R., Kuncak, V.: Collections, cardinalities, and relations. In: Barthe, G., Hermenegildo, M. (eds.) VMCAI 2010. LNCS, vol. 5944, pp. 380–395. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this paper
Cite this paper
Alberti, F., Ghilardi, S., Pagani, E. (2016). Counting Constraints in Flat Array Fragments. In: Olivetti, N., Tiwari, A. (eds) Automated Reasoning. IJCAR 2016. Lecture Notes in Computer Science(), vol 9706. Springer, Cham. https://doi.org/10.1007/978-3-319-40229-1_6
Download citation
DOI: https://doi.org/10.1007/978-3-319-40229-1_6
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-40228-4
Online ISBN: 978-3-319-40229-1
eBook Packages: Computer ScienceComputer Science (R0)