kirancodes.me
To Proof Maintenance & Beyond!
FSE 2020

MCBAT: a practical tool for model counting constraints on bounded integer arrays

Abtin Molavi, Mara Downing, Tommy Schneider, Lucas Bang

PDFDOI 10.1145/3368089.3417937dblp

Abstract

Model counting procedures for data structures are crucial for advancing the field of automated quantitative program analysis. We present a tool for Model Counting for Bounded Array Theory (MCBAT). MCBAT works on 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). Once reduced to LIA, we leverage Barvinok's polynomial time integer lattice point enumeration algorithm. Finally, we present a case study demonstrating applicability to automated quantitative program analysis. MCBAT is available for immediate use as a Docker image and the source code is freely available in our Github repository.

BibTeX
@inproceedings{Molavi-al:FSE20,
  author    = {Abtin Molavi and
               Mara Downing and
               Tommy Schneider and
               Lucas Bang},
  title     = {{MCBAT:} a practical tool for model counting constraints on bounded integer arrays},
  booktitle = {{ESEC/SIGSOFT} {FSE}},
  pages     = {1596--1600},
  publisher = {{ACM}},
  year      = {2020},
}

Related papers