January 18 (Wednesday) 3:30PM
Seminar Hall
Towards Building A Scalable Bitvector Model Counter
Arijit Shaw
Chennai Mathematical Institute and IAI, TCG-CREST.
18-01-23

---

Abstract

The widespread use of Satisfiability Modulo Theory (SMT) solvers in automated reasoning has led to the investigation of their potential for solving problems beyond satisfiability. Propositional model counting has recently seen significant progress, and are being utilized to solve complex quantitative problems in various research areas, including model checking, software verification, cryptography, machine learning, and computational biology. These applications inspire the development of scalable counters for SMT. In this talk, we will present our work on developing a scalable model counting system for the theory of quantifier-free bit-vector (QFBV) arithmetic called SharpSMT. This system uses a portfolio approach that combines propositionalization techniques, preprocessors, and off-the-shelf model counting tools. Our experiments using a diverse set of benchmarks from various research domains show that SharpSMT performs 4 times better than the current state-of-the-art.

This work is a part of Arijit’s PhD work and is a work in progress.