Skip to main content
SpringerLink
Log in

MCBAT: Model Counting for Constraints over Bounded Integer Arrays

  • Conference paper
  • First Online:
Software Verification (NSV 2020, VSTTE 2020)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 12549))

Abstract

Model counting procedures for data structures are crucial for advancing the field of automated quantitative program analysis. We present an algorithm and practical tool for performing Model Counting for Bounded Array Theory (MCBAT). As the satisfiability problem for the theory of arrays is undecidable in general, we focus on a fragment of array theory for which we are able to specify an exact model counting algorithm. MCBAT applies to quantified integer array constraints in which all arrays have a finite length. We employ reductions from the theory of arrays to uninterpreted functions and linear integer arithmetic (LIA), and we prove these reductions to be model-count preserving. Once reduced to LIA, we leverage Barvinok’s polynomial time integer lattice point enumeration algorithm. Finally, we present experimental validation for the correctness and scalability of our approach and apply MCBAT to a case study on automated average case analysis for array programs, demonstrating applicability to automated quantitative program analysis.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • 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

Notes

  1. 1.

    Note to reviewers: our implementation and experiments are ready for immediate public release upon publication of our results.

References

  1. Ackermann, W.: Solvable Cases of the Decision Problem. North-Holland Pub. Co., Amsterdam (1954)

    MATH  Google Scholar 

  2. Aydin, A., Bang, L., Bultan, T.: Automata-based model counting for string constraints. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 255–272. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-21690-4_15

    Chapter  Google Scholar 

  3. Aydin, A., et al.: Parameterized model counting for string and numeric constraints. In: Proceedings of the 2018 ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/SIGSOFT FSE 2018, Lake Buena Vista, FL, USA, 04–09 November 2018, pp. 400–410 (2018)

    Google Scholar 

  4. Barvinok, A.I.: A polynomial time algorithm for counting integral points in polyhedra when the dimension is fixed. Math. Oper. Res. 19(4), 769–779 (1994)

    Article  MathSciNet  Google Scholar 

  5. Belle, V.: Weighted model counting with function symbols. In: Proceedings of the Thirty-Third Conference on Uncertainty in Artificial Intelligence, UAI 2017, Sydney, Australia, 11–15 August 2017 (2017)

    Google Scholar 

  6. Birnbaum, E., Lozinskii, E.L.: The good old Davis-Putnam procedure helps counting models. J. Artif. Int. Res. 10(1), 457–477 (1999)

    Google Scholar 

  7. Borges, M., Phan, Q.-S., Filieri, A., Păsăreanu, C.S.: Model-counting approaches for nonlinear numerical constraints. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 131–138. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-57288-8_9

    Chapter  Google Scholar 

  8. 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 

  9. Chakraborty, S., Meel, K., Mistry, R., Vardi, M.: Approximate probabilistic inference via word-level counting, November 2015

    Google Scholar 

  10. Chavira, M., Darwiche, A.: On probabilistic inference by weighted model counting. Artif. Intell. 172(6), 772–799 (2008)

    Article  MathSciNet  Google Scholar 

  11. De Salvo Braz, R., O’Reilly, C., Gogate, V., Dechter, R.: Probabilistic inference modulo theories. In: Proceedings of the Twenty-Fifth International Joint Conference on Artificial Intelligence, IJCAI 2016, pp. 3591–3599. AAAI Press (2016)

    Google Scholar 

  12. Eiers, W., Saha, S., Brennan, T., Bultan, T.: Subformula caching for model counting and quantitative program analysis. In: Proceedings of The 34th IEEE/ACM International Conference on Automated Software Engineering ASE (2019)

    Google Scholar 

  13. Filieri, A., Frias, M.F., Păsăreanu, C.S., Visser, W.: Model counting for complex data structures. In: Fischer, B., Geldenhuys, J. (eds.) SPIN 2015. LNCS, vol. 9232, pp. 222–241. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-23404-5_15

    Chapter  Google Scholar 

  14. Filieri, A., Pasareanu, C.S., Visser, W.: Reliability analysis in symbolic pathfinder. In: 35th International Conference on Software Engineering, ICSE 2013, San Francisco, CA, USA, 18–26 May 2013, pp. 622–631 (2013)

    Google Scholar 

  15. Flajolet, P., Salvy, B., Zimmermann, P.: Automatic average-case analysis of algorithm. Theor. Comput. Sci. 79(1), 37–109 (1991)

    Article  MathSciNet  Google Scholar 

  16. Fromherz, A., Luckow, K.S., Pasareanu, C.S.: Symbolic arrays in symbolic pathfinder. ACM SIGSOFT Softw. Eng. Notes 41(6), 1–5 (2016)

    Article  Google Scholar 

  17. Geldenhuys, J., Dwyer, M.B., Visser, W.: Probabilistic symbolic execution. In: Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA 2012, pp. 166–176. ACM, New York (2012)

    Google Scholar 

  18. Klebanov, V.: Precise quantitative information flow analysis - a symbolic approach. Theor. Comput. Sci. 538, 124–139 (2014)

    Article  MathSciNet  Google Scholar 

  19. Kroening, D., Strichman, O.: Decision Procedures: An Algorithmic Point of View, 1st edn. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-74105-3

    Book  MATH  Google Scholar 

  20. Larraz, D., Rodríguez-Carbonell, E., Rubio, A.: SMT-based array invariant generation. In: Giacobazzi, R., Berdine, J., Mastroeni, I. (eds.) VMCAI 2013. LNCS, vol. 7737, pp. 169–188. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35873-9_12

    Chapter  Google Scholar 

  21. Loera, J.A.D., Hemmecke, R., Tauzer, J., Yoshida, R.: Effective lattice point counting in rational convex polytopes. J. Symb. Comput. 38(4), 1273–1302 (2004)

    Article  MathSciNet  Google Scholar 

  22. Luu, L., Shinde, S., Saxena, P., Demsky, B.: A model counter for constraints over unbounded strings. In: Proceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2014, pp. 565–576. ACM, New York (2014)

    Google Scholar 

  23. Malacaria, P., Khouzani, M.H.R., Pasareanu, C.S., Phan, Q., Luckow, K.S.: Symbolic side-channel analysis for probabilistic programs. In: 31st IEEE Computer Security Foundations Symposium, CSF 2018, Oxford, United Kingdom, 9–12 July 2018, pp. 313–327 (2018)

    Google Scholar 

  24. McCarthy, J.: Towards a mathematical science of computation. In: Colburn, T.R., Fetzer, J.H., Rankin, T.L. (eds.) Information Processing. SCS, vol. 14, pp. 21–28. Springer, Dordrecht (1962). https://doi.org/10.1007/978-94-011-1793-7_2

    Chapter  Google Scholar 

  25. 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 

  26. de Moura, L.M., Bjørner, N.: Generalized, efficient array decision procedures. In: Proceedings of 9th International Conference on Formal Methods in Computer-Aided Design, FMCAD 2009, 15–18 November 2009, Austin, Texas, USA pp. 45–52 (2009)

    Google Scholar 

  27. Phan, Q., Malacaria, P., Pasareanu, C.S., d’Amorim, M.: Quantifying information leaks using reliability analysis. In: 2014 International Symposium on Model Checking of Software, SPIN 2014, Proceedings, San Jose, CA, USA, 21–23 July 2014, pp. 105–108 (2014)

    Google Scholar 

  28. Plazar, Q., Acher, M., Bardin, S., Gotlieb, A.: Efficient and complete fd-solving for extended array constraints, pp. 1231–1238, August 2017

    Google Scholar 

  29. Pugh, W.: Counting solutions to Presburger formulas: how and why. In: Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, PLDI 1994, pp. 121–134. ACM, New York (1994)

    Google Scholar 

  30. Sang, T., Bearne, P., Kautz, H.: Performing bayesian inference by weighted model counting. In: Proceedings of the 20th National Conference on Artificial Intelligence, AAAI 2005, vol. 1, pp. 475–481. AAAI Press (2005)

    Google Scholar 

  31. Sherman, E., Harris, A.: Accurate string constraints solution counting with weighted automata. In: Proceedings of The 34th IEEE/ACM International Conference on Automated Software Engineering ASE (2019)

    Google Scholar 

  32. Trinh, M.-T., Chu, D.-H., Jaffar, J.: Model counting for recursively-defined strings. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10427, pp. 399–418. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63390-9_21

    Chapter  Google Scholar 

  33. Tsiskaridze, N., Bang, L., McMahan, J., Bultan, T., Sherwood, T.: Information leakage in arbiter protocols. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 404–421. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_24

    Chapter  Google Scholar 

  34. Verdoolaege, S., Seghir, R., Beyls, K., Loechner, V., Bruynooghe, M.: Counting integer points in parametric polytopes using Barvinok’s rational functions. Algorithmica 48(1), 37–66 (2007)

    Google Scholar 

  35. Visser, W., Pasareanu, C.S.: Probabilistic programming for Java using symbolic execution and model counting. In: Proceedings of the South African Institute of Computer Scientists and Information Technologists, SAICSIT 2017, Thaba Nchu, South Africa, 26–28 September 2017, pp. 35:1–35:10 (2017)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Harvey Mudd College, Claremont, CA, 91711, USA

    Abtin Molavi, Tommy Schneider, Mara Downing & Lucas Bang

Authors
  1. Abtin Molavi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Tommy Schneider
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Mara Downing
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Lucas Bang
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Lucas Bang .

Editor information

Editors and Affiliations

  1. MPI-SWS Kaiserslautern, Kaiserslautern, Germany

    Maria Christakis

  2. University of California, San Diego, La Jolla, CA, USA

    Nadia Polikarpova

  3. Computer Science, University of North Carolina at Chapel Hill, Chapel Hill, NC, USA

    Parasara Sridhar Duggirala

  4. Engineering and Informatics, University of Sussex, Brighton, UK

    Peter Schrammel

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Molavi, A., Schneider, T., Downing, M., Bang, L. (2020). MCBAT: Model Counting for Constraints over Bounded Integer Arrays. In: Christakis, M., Polikarpova, N., Duggirala, P.S., Schrammel, P. (eds) Software Verification. NSV VSTTE 2020 2020. Lecture Notes in Computer Science(), vol 12549. Springer, Cham. https://doi.org/10.1007/978-3-030-63618-0_8

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-63618-0_8

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-63617-3

  • Online ISBN: 978-3-030-63618-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation