Scalable Model Counting for Program Analysis

Abstract

Various model counting techniques have been proposed to show their scalability for problem domains such as combinatorics, safety analysis, probabilistic inference and quantitative information-flow analysis of software. In particular, random hashing-based methods have shown to be highly successful in computing bounds on the model count of a propositional formula. These hashing-based algorithms repeatedly check the satisfiability of a formula subject to random parity constraints (XOR streamlining) and give an estimate of the model count with a probabilistic range and confidence. However, these approaches often perform poorly when the size of parity constraints becomes too large and/or the complexity of the formula increases because they are highly dependent on the performance of a decision procedure. In this thesis, we focus on increasing scalability of hashing-based model counting techniques and applying the model counting techniques to analyze programs. This thesis is divided into three parts. We first describe two efficient approximate model counting tools: SearchMC and SMC. SearchMC is a hashing-based approximate model counter which uses fruitful SAT/SMT queries to compute a lower bound and an upper bound based on statistical estimation, and yields results more quickly than existing systems. SMC is a structural model counter which analyzes the structure of a formula to compute firm lower and upper bounds in polynomial time. Moreover, we can use SMC to compute a refined initial hypothesis without any solver calls for SearchMC. Secondly, we explain a divide-and-conquer algorithm, MultiSearchMC, to increase scalability of hashing-based model counting techniques using parallelization. We first split an input formula into small formulae and run the combination of SMC and SearchMC in parallel. Then, we conservatively combine all the results to compute an estimate of the model count. Lastly, we analyze realistic programs using this improved model counting technique. We show how we can apply model counting techniques to quantitative information flow analysis and uniform sampling for testing. Also, the experimental results illustrate that our approach is able to handle large-sized input/output data for quantitative information flow analysis and uniform sampling in certain domains.