Supratik Chakraborty

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

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.

I'm also affiliated to Centre for Formal Design and Verification of Software and Centre for Liberal Education at IIT Bombay.


My current research interests include:

Selected Talks/Tutorials

Selected recent publications

[For a complete listing of publications, see here ]

Doctoral students

1   Joycee Mekie , now at IIT Gandhinagar
(co-supervised with Dinesh K. Sharma )
Interfacing Solutions for Globally Asynchronous Locally Synchronous (GALS) Systems (graduated 2009)
2 Bhargav Gulavani, now at Microsoft Research On Improving the Precision of Static Program Analysis (graduated 2010, IIT Bombay Excellence in Thesis (CSE) Award 2011)
3 Hrishikesh Karmarkar , now at TCS Research Improved Constructions for Complementation, Disambiguation and Determinization of ω-automata (graduated 2011)
4 Seetha Jayasankar Reachability Analysis of Large Sequential Circuits (on leave)
5 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)
6 Ajith K. John, now at BARC Scalable Quantifier Elimination Techniques for Formal Verification (graduated 2017)
7 Kuldeep Singh Meel , now at University of Toronto
(co-supervised with Moshe Y. Vardi, Rice University)
Constrained Counting and Sampling: Bridging the Gap between Theory and Practice (graduated 2017)
8 Sukanya Basu
(co-supervised with Akshay S.)
Functional Significance Checking in Biological Networks: Theory and Implementation (graduated 2020)
9 Divyesh Unadkat, now at Synopsys Inc.
(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 ...

Web Analytics Made Easy - Statcounter