Arijit Shaw: Measuring Solution Spaces: Scalable Quantitative Reasoning in SMT

HIIT Special Seminars
This talk is part of the HIIT Special Seminar series. The talks in this series are provided by candidates who have applied to our HIIT Fellowship recruitment call and are highly considered for the position. All talks are virtual, open to the public, and recorded for the future.
HIIT Special Seminar

When

–

Where

Online

Event language(s)

English
Join via zoom

This talk can be viewed via zoom. (Note: this talk will be recorded)

Title: Measuring Solution Spaces: Scalable Quantitative Reasoning in SMT

Abstract: In a stochastic system, what is the probability of violating a safety property? How reliable are our power grids in a disaster scenario? Classically, automated reasoning addressed such questions for deterministic systems by reducing them to satisfiability queries, asking whether a solution exists. But as systems increasingly operate under uncertainty, a yes/no answer is no longer enough: the right question is not whether a solution exists, but how large the solution space is. This talk addresses these questions through quantitative automated reasoning, casting them as measure problems in Satisfiability Modulo Theories (SMT). Building on  randomized algorithms, we show how these measure problems can be solved scalably.


Bio: Arijit Shaw is a final year Ph.D. student at the Chennai Mathematical Institute, advised by Kuldeep Meel, working on the field of automated reasoning. He received the Best Student Paper Award at KR, organizes the Model Counting Competition, and has won awards at the SAT Competition.

  • Updated:
  • Published:
Share
URL copied!