MCBAT: Model Counting for Constraints over Bounded Integer Arrays

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.