Scalable Model Counting for Program Analysis

Thumbnail Image

Persistent link to this item

View Statistics

Journal Title

Journal ISSN

Volume Title


Scalable Model Counting for Program Analysis

Published Date




Thesis or Dissertation


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.


University of Minnesota Ph.D. dissertation. 2022. Major: Computer Science. Advisor: Stephen McCamant. 1 computer file (PDF); 111 pages.

Related to




Series/Report Number

Funding information

Isbn identifier

Doi identifier

Previously Published Citation

Suggested citation

Kim, Seonmo. (2022). Scalable Model Counting for Program Analysis. Retrieved from the University Digital Conservancy,

Content distributed via the University Digital Conservancy may be subject to additional license and use restrictions applied by the depositor. By using these files, users agree to the Terms of Use. Materials in the UDC may contain content that is disturbing and/or harmful. For more information, please see our statement on harmful content in digital repositories.