Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
A Logical Framework for Developing and Mechanizing Set Theories Kapitel lesen Erstes Kapitel lesen

2016 | OriginalPaper | Buchkapitel

Counting Constraints in Flat Array Fragments

verfasst von : Francesco Alberti, Silvio Ghilardi, Elena Pagani

Erschienen in: Automated Reasoning

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Super-Blocked Clauses
Nächstes Kapitel A New Decision Procedure for Finite Sets and Cardinality Constraints in SMT
Fußnoten
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.
 
Literatur
1.
Alberti, F., Ghilardi, S., Pagani, E.: Counting constraints in flat array fragments (2016). CoRR, abs/1602.00458
2.
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)CrossRef
3.
Biely, M., Charron-Bost, B., Gaillard, A., Hutle, M., Schiper, A., Widder, J.: Tolerating corrupted communication. In: Proceedings of PODC, pp. 244–253 (2007)
4.
5.
Charron-Bost, B., Schiper, A.: The heard-of model: computing in distributed systems with benign faults. Distrib. Comput. 22, 49–71 (2009)CrossRefMATH
6.
Dijkstra, E.W.: Cooperating sequential processes. In: Genuys, F. (ed.) Programming Languages, pp. 43–112. Academic Press, New York (1968)
7.
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)CrossRef
8.
Dragoi, C., Henzinger, T.A., Zufferey, D.: The need for language support for fault-tolerant distributed systems. In: Proceedings of SNAPL (2015)
9.
10.
Halpern, J.Y.: Presburger arithmetic with unary predicates is \(\Pi ^1_1\) complete. J. Symbol. Logic 56(2), 637–642 (1991)CrossRefMATH
11.
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
12.
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)
13.
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)CrossRef
14.
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)CrossRef
15.
Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding boolean algebra with Presburger arithmetic. J. Autom. Reasoning 36(3), 213–239 (2006)MathSciNetCrossRefMATH
16.
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)CrossRef
17.
Papamarcos, M.S., Patel, J.H.: A low-overhead coherence solution for multiprocessors with private cache memories. In: Proceedings of ISCA, p. 348 (1984)
18.
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)CrossRef
19.
Schweikhart, N.: Arithmetic, first-order logic, and counting quantifiers. ACM TOCL 6, 1–35 (2004)
20.
Solihin, Y.: Fundamentals of Parallel Computer Architecture Multichip and Multicore Systems. Solihin Publishing & Consulting LLC (2008)
21.
22.
Srikanth, T.K., Toueg, S.: Simulating authenticated broadcasts to derive simple fault-tolerant algorithms. Distrib. Comput. 2(2), 80–94 (1987)CrossRef
23.
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)CrossRef
Metadaten
Titel
Counting Constraints in Flat Array Fragments
verfasst von
Francesco Alberti
Silvio Ghilardi
Elena Pagani
Copyright-Jahr
2016
Buch
Automated Reasoning

Print ISBN: 978-3-319-40228-4

Electronic ISBN: 978-3-319-40229-1

Copyright-Jahr: 2016

DOI
https://doi.org/10.1007/978-3-319-40229-1_6

Premium Partner

    Bildnachweise