Supratik Chakraborty

I work in the area of formal methods, developing theory, algorithms and computational tools that help in building verifiably correct hardware, software and intelligent systems. Such systems increasingly pervade our lives, yet their growing complexity makes it humanly impossible to reason about all corner case behaviours. Mathematically provable guarantees are therefore crucial to ensure that the systems we increasingly trust our lives on are indeed trustworthy.
My research focuses on (i) formal verification, wherein we provide a formal proof that a system satisfies a property or demonstrate its violation, (ii) rigorous analysis of system models to extract meaningful information, and (iii) automated synthesis of systems from specifications, with the guarantee that the synthesized system satisfies the specification.
I have applied formal methods to reason about software, hardware, machine learning and biological systems. The gap between theory and practice of formal methods concerns me deeply and I have consciously tried to bridge this gap in my work.

Research

Constrained counting and sampling, and their applications

Scalable formal verification of software, hardware and intelligent systems

Automated synthesis of programs and circuits

Automated reasoning

Automata, logic and finite model theory

Selected Talks/Tutorials

Automated Synthesis: Towards the Holy Grail of AI", tutorial co-presented with Kuldeep S. Meel, Akshay S., P. Golia and S. Roy at AAAI 2022 and IJCAI 2022

Three talks on "Boolean Functional Synthesis" at Simons Institute for the Theory of Computing, 2021

"Algorithms for Boolean Functional Synthesis" [Slides]
"Knowledge Compilation for Boolean Functional Synthesis" [Slides] [Video]
"Counterexample Guided Repair in Boolean Functional Synthesis" [Slides] [Video]

"Scaling Discrete Integration and Sampling: Foundations and Challenges", tutorial co-presented with Kuldeep S. Meel at IJCAI 2018

"Abstract Interpretation and Program Verification", tutorial presented at ACM ISOFT Winter School on Software Engineering [Slides]

"Discrete Sampling and Counting for the AI Practitioner", tutorial co-presented with Kuldeep S. Meel and Moshe Y. Vardi at AAAI 2017

"Counting and Sampling Solutions of SAT/SMT Constraints", invited talk at International Summer School on Satisfiabilty, Satisfiability Modulo Theories and Automated Reasoning 2016

"Discrete Sampling and Integration in High Dimensional Spaces", tutorial co-presented with Kuldeep S. Meel and Moshe Y. Vardi at UAI 2016

"Word-level Quantifier Elimination", invited talk at VMCAI 2015 [ Slides ]

Selected recent publications

here

S. Akshay and S. Chakraborty, "Synthesizing Skolem functions: A view from theory and practice", in Handbook of Logical Thought in India, eds. Sundar Sarukkai and Mihir K. Chakraborty, Springer, Jule 2022 [PDF of chapter preprint] (The published chapter can be found on Springer Link).

S. Chakraborty, K.S. Meel and M.Y. Vardi, "Approximate Model Counting", book chapter in Handbook of Satisfiability, 2nd edition, eds. Armin Biere, Marijn Heule, Hans van Maaren and Toby Walsh, IOS Press, Feb 2021 [PDF of chapter preprint]. (The print edition can be ordered here. The published electronic chapters (Version of Record) are available here).

S. Chakraborty and S. Akshay, "On Synthesizing Computable Skolem Functions for First Order Logic", in Proc. of International Conference on Mathematical Foundations of Computer Science, pages 30:1-30:15, Aug 2022 [PDF]

H. Torfah, S. Shah, S. Chakraborty, S. Akshay and S. Seshia, "Synthesizing Pareto-optimal Interpretations for Black-Box Models", in Proc. of International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 153-162, Oct 2021 [PDF of extended version on arXiv.org]

S. Chakraborty, A. Gupta and D. Unadkat, "Diffy: Inductive Reasoning of Array Programs using Difference Invariants", in Proc. of International Conference on Computer-Aided Verification (CAV), pages 911-935, Jul 2021 [PDF of extended version on arXiv.org]

P. Shah, A. Bansal, S. Akshay and S. Chakraborty, "A Normal Form Characterization for Efficient Boolean Skolem Function Synthesis", in Proc. of International Symposium on Logic in Computer Science (LICS), pages 1--13, Jul 2021 [PDF of extended version on arXiv.org]

S. Akshay, S. Chakraborty, S. Goel, S. Kulal and S. Shah, "Boolean Functional Synthesis: Hardness and Practical Algorithms", in Formal Methods in System Design, Vol 57(1), pages 53--86, 2021 (published online Oct 2020 at Springer SharedIt) [PDF of pre-print]

S. Chakraborty, A. Gupta and D. Unadkat, "Verifying Array Manipulating Programs with Full-Program Induction", in Proc. of International Conference on Tools and Algorithms for Construction and Analysis of Systems (TACAS), pages 22-39, Apr 2020 [Springer Open Access]

Doctoral students

Joycee Mekie , now at IIT Gandhinagar
(co-supervised with Dinesh K. Sharma )

Interfacing Solutions for Globally Asynchronous Locally Synchronous (GALS) Systems (graduated 2009)

Bhargav Gulavani, now at Microsoft Research

On Improving the Precision of Static Program Analysis (graduated 2010, IIT Bombay Excellence in Thesis (CSE) Award 2011)

Hrishikesh Karmarkar , now at TCS Research

Improved Constructions for Complementation, Disambiguation and Determinization of ω-automata (graduated 2011)

Seetha Jayasankar

Reachability Analysis of Large Sequential Circuits (on leave)

Abhisekh Sankaran, now at TCS Research
(co-supervised with Bharat Adsul )

A Generalization of the Łoś-Tarski Preservation Theorem (graduated 2016, IIT Bombay Excellence in Thesis (CSE) Award 2017)

Ajith K. John, now at BARC

Scalable Quantifier Elimination Techniques for Formal Verification (graduated 2017)

Kuldeep Singh Meel , now at National University of Singapore
(co-supervised with Moshe Y. Vardi, Rice University)

Constrained Counting and Sampling: Bridging the Gap between Theory and Practice (graduated 2017)

Sukanya Basu
(co-supervised with Akshay S.)

Functional Significance Checking in Biological Networks: Theory and Implementation (graduated 2020)

Divyesh Unadkat, now at TCS Research
(co-supervised with Ashutosh Gupta)

Inductive Reasoning for Precise and Scalable Verification of Array Programs (graduated 2023)

Last but not the least, alumni and their contributions to our research efforts.

On a lighter note, some ideas for business plans ...

	Supratik Chakraborty
	Bajaj Group Chair Professor Department of Computer Science and Engineering Indian Institute of Technology Bombay