MCBAT: Model Counting for Constraints over Bounded Integer Arrays

Autor:	Lucas Bang, Mara Downing, Abtin Molavi, Tommy Schneider
Rok vydání:	2020
Předmět:	Program analysis Correctness Computer science Bounded function Integer lattice Boolean satisfiability problem Time complexity Algorithm Undecidable problem Integer (computer science)
Zdroj:	Lecture Notes in Computer Science ISBN: 9783030636173 VSTTE
Popis:	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.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::0138ea90ba81aea7c62adedfbb6d7610 https://doi.org/10.1007/978-3-030-63618-0_8 Zobrazit plný text záznamu