arijit

Speaker: Arijit Shaw 

Date: May 17th, 2023

Time: 3:30 pm

Location: HFH 1132

Host: Tevfik Bultan 

Title: Building a Scalable bit-vector model counter

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 made significant progress, inspiring the development of scalable counters for SMT.
In this talk, we will present our work on developing a scalable model counting system for SMT theory of quantifier-free bit-vector (QFBV) arithmetic. Our approach utilizes word-level hash functions and sophisticated SMT solvers to efficiently handle model count hard formulas. We will also provide examples from different domains that demonstrate the utility of model counting tools for addressing various quantitative questions.

Bio:


Arijit is a third-year Ph.D. student at the Chennai Mathematical Institute. His research interests lie in the field of formal methods, and he is particularly interested in designing scalable solutions for problems that lie beyond the complexity class of NP. His current focus is on designing model counters for different SMT theories, and he is advised by Dr. Kuldeep S. Meel of NUS, Singapore.

Prior to beginning his PhD studies, Arijit completed his M.Sc. at the Chennai Mathematical Institute and his B.Tech. at Jadavpur University. He has also achieved success in the field of SAT solvers, having won prizes in the SAT Competition 2020 and the EDA Challenge 2021.