NP Satisfiability for Arrays as Powers | SpringerLink
Skip to main content
Springer Nature Link
Log in

NP Satisfiability for Arrays as Powers

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2022)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 13182))

  • 1098 Accesses

Abstract

We show that the satisfiability problem for the quantifier-free theory of product structures with the equicardinality relation is in NP. As an application, we extend the combinatory array logic fragment to handle cardinality constraints. The resulting fragment is independent of the base element and index set theories.

Research supported in part by the Swiss NSF Project #200021_197288.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 10295
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 12869
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

References

  1. Alberti, F., Ghilardi, S., Pagani, E.: Cardinality constraints for arrays (decidability results and applications). Formal Methods Syst. Des. 51(3), 545–574 (2017). https://doi.org/10.1007/s10703-017-0279-6

    Article  MATH  Google Scholar 

  2. Alberti, F.: An SMT-based verification framework for software systems handling arrays. Ph.D. thesis, Università della Svizzera Italiana, April 2015. http://www.falberti.it/thesis/phd.pdf

  3. Alberti, F., Ghilardi, S., Sharygina, N.: Decision procedures for flat array properties. J. Autom. Reason. 54(4), 327–352 (2015). https://doi.org/10.1007/s10817-015-9323-7

    Article  MathSciNet  MATH  Google Scholar 

  4. Bradley, A.R., Manna, Z., Sipma, H.B.: What’s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) VMCAI 2006. LNCS, vol. 3855, pp. 427–442. Springer, Heidelberg (2005). https://doi.org/10.1007/11609773_28

    Chapter  Google Scholar 

  5. Daca, P., Henzinger, T.A., Kupriyanov, A.: Array folds logic. In: Chaudhuri, S., Farzan, A. (eds.) CAV 2016. LNCS, vol. 9780, pp. 230–248. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-41540-6_13

    Chapter  Google Scholar 

  6. Eisenbrand, F., Shmonin, G.: Carathéodory bounds for integer cones. Oper. Res. Lett. 34(5), 564–568 (2006). https://doi.org/10.1016/j.orl.2005.09.008

    Article  MathSciNet  MATH  Google Scholar 

  7. Feferman, S., Vaught, R.: The first order properties of products of algebraic systems. Fundam. Math. 47(1), 57–103 (1959). https://eudml.org/doc/213526

  8. Ferrante, J., Rackoff, C.W.: The Computational Complexity of Logical Theories. Lecture Notes in Mathematics, vol. 718. Springer, Heidelberg (1979). https://doi.org/10.1007/BFb0062837

    Book  MATH  Google Scholar 

  9. von zur Gathen, J., Sieveking, M.: A bound on solutions of linear integer equalities and inequalities. Proc. Am. Math. Soc. 72(1), 155–158 (1978). https://doi.org/10.2307/2042554

    Article  MathSciNet  MATH  Google Scholar 

  10. Ghilardi, S., Nicolini, E., Ranise, S., Zucchelli, D.: Decision procedures for extensions of the theory of arrays. Ann. Math. Artif. Intell. 50(3), 231–254 (2007). https://doi.org/10.1007/s10472-007-9078-x

    Article  MathSciNet  MATH  Google Scholar 

  11. Grädel, E.: Dominoes and the complexity of subclasses of logical theories. Ann. Pure Appl. Logic 43(1), 1–30 (1989). https://doi.org/10.1016/0168-0072(89)90023-7

    Article  MathSciNet  MATH  Google Scholar 

  12. Habermehl, P., Iosif, R., Vojnar, T.: What else is decidable about integer arrays? In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 474–489. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78499-9_33

    Chapter  Google Scholar 

  13. Hodges, W.: Model Theory. Encyclopedia of Mathematics and its Applications, Cambridge University Press, Cambridge (1993). https://doi.org/10.1017/CBO9780511551574

    Book  MATH  Google Scholar 

  14. Kuncak, V., Nguyen, H.H., Rinard, M.: Deciding Boolean algebra with Presburger arithmetic. J. Autom. Reason. 36(3), 213–239 (2006). https://doi.org/10.1007/s10817-006-9042-1

    Article  MathSciNet  MATH  Google Scholar 

  15. Kuncak, V., Piskac, R., Suter, P.: Ordered sets in the calculus of data structures. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 34–48. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15205-4_5

    Chapter  Google Scholar 

  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). https://doi.org/10.1007/978-3-540-73595-3_15

    Chapter  Google Scholar 

  17. McCarthy, J.: Towards a mathematical science of computation. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Program Verification: Fundamental Issues in Computer Science. Studies in Cognitive Systems, pp. 35–56. Springer, Dordrecht (1993). https://doi.org/10.1007/978-94-011-1793-7_2

    Chapter  Google Scholar 

  18. Mostowski, A.: On direct products of theories. J. Symbol. Logic 17(1), 1–31 (1952). https://doi.org/10.2307/2267454

    Article  MathSciNet  MATH  Google Scholar 

  19. de Moura, L., Bjorner, N.: Generalized, efficient array decision procedures. In: 2009 Formal Methods in Computer-Aided Design, Austin, TX, pp. 45–52. IEEE, November 2009. https://doi.org/10.1109/FMCAD.2009.5351142

  20. de Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78800-3_24

    Chapter  Google Scholar 

  21. Stump, A., Barrett, C., Dill, D., Levitt, J.: A decision procedure for an extensional theory of arrays. In: Proceedings 16th Annual IEEE Symposium on Logic in Computer Science, Boston, MA, USA, pp. 29–37. IEEE Computer Society (2001). https://doi.org/10.1109/LICS.2001.932480

Download references

Author information

Authors and Affiliations

  1. School of Computer and Communication Science, École Polytechnique Fédérale de Lausanne (EPFL), Lausanne, Switzerland

    Rodrigo Raya & Viktor Kunčak

Authors
  1. Rodrigo Raya
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Viktor Kunčak
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Rodrigo Raya .

Editor information

Editors and Affiliations

  1. Helmholtz Center for Information Security, Saarbrücken, Germany

    Bernd Finkbeiner

  2. New York University, New York, NY, USA

    Thomas Wies

Rights and permissions

Reprints and permissions

Copyright information

© 2022 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Raya, R., Kunčak, V. (2022). NP Satisfiability for Arrays as Powers. In: Finkbeiner, B., Wies, T. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2022. Lecture Notes in Computer Science(), vol 13182. Springer, Cham. https://doi.org/10.1007/978-3-030-94583-1_15

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-94583-1_15

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-94582-4

  • Online ISBN: 978-3-030-94583-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation