ESEC/FSE 2020 (series) / Tool Demos /
MCBAT: A Practical Tool for Model Counting Constraints on Bounded Integer Arrays
Fri 13 Nov 2020 01:37 - 01:38 at Virtual room 2 - SAT and Synthesis
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.
Fri 13 Nov Times are displayed in time zone: (UTC) Coordinated Universal Time change
Fri 13 Nov
Times are displayed in time zone: (UTC) Coordinated Universal Time change
01:30 - 02:00: SAT and SynthesisPaper Presentations / Research Papers / Tool Demos at Virtual room 2 | |||
| 01:30 - 01:32 Talk | AlloyMC: Alloy Meets Model Counting Tool Demos Jiayi YangUniversity of Texas at Austin, USA, Wenxi WangUniversity of Texas at Austin, USA, Darko MarinovUniversity of Illinois at Urbana-Champaign, Sarfraz KhurshidUniversity of Texas at Austin DOI | ||
| 01:32 - 01:34 Talk | HISyn: Human Learning-Inspired Natural Language Programming Research Papers Zifan NanNorth Carolina State University, USA, Hui GuanUniversity of Massachusetts at Amherst, USA, Xipeng ShenNorth Carolina State University, USA DOI | ||
| 01:35 - 01:36 Talk | Inductive Program Synthesis over Noisy Data Research Papers Shivam HandaMassachusetts Institute of Technology, USA, Martin RinardMassachusetts Institute of Technology, USA DOI | ||
| 01:37 - 01:38 Talk | MCBAT: A Practical Tool for Model Counting Constraints on Bounded Integer Arrays Tool Demos Abtin MolaviHarvey Mudd College, USA, Mara DowningHarvey Mudd College, USA, Tommy SchneiderHarvey Mudd College, USA, Lucas BangHarvey Mudd College DOI | ||
| 01:39 - 01:40 Talk | SVMRanker: A General Termination Analysis Framework of Loop Programs via SVM Tool Demos Xie Li, Yi LiNanyang Technological University, Singapore, Yong LiInstitute of Software, Chinese Academy of Sciences, Xuechao SunInstitute of Software at Chinese Academy of Sciences, China, Andrea TurriniState Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Lijun ZhangInstitute of Software, Chinese Academy of Sciences DOI | ||
| 01:41 - 02:00 Talk | Conversations on SAT and Synthesis Paper Presentations Abtin MolaviHarvey Mudd College, USA, Jiayi YangUniversity of Texas at Austin, USA, Lucas BangHarvey Mudd College, Xie Li, Zifan NanNorth Carolina State University, USA, Shivam HandaMassachusetts Institute of Technology, USA, M: Abhik RoychoudhuryNational University of Singapore, Singapore | ||