| M. Tech. | Debtanu Pal (co-supervised with S. Akshay ) |
On Eventual Properties of Sets of Matrices |
| Nikhil Durgam (co-supervised with Amitabha Sanyal ) |
RTL Translation Validation |
| Ph.D. | Sukanya Basu (co-supervised with Akshay S. ) |
Functional Significance Checking in Biological Networks: Theory and Implementation |
| M. Tech. | Ananya Bahadur (co-supervised with Amitabha Sanyal ) |
Abstraction based Translation Validation of GCC's Tree Optimizations |
| Ajeesh Kumar K (co-supervised with Amitabha Sanyal ) |
RTL Translation Validation | |
| B. Tech. | Preey Shah (co-supervised with Akshay S. ) |
On Extensions of Synthesis Negation Normal Form |
| Aman Bansal (co-supervised with Akshay S. ) |
On Extensions of Synthesis Negation Normal Form |
| M. Tech. | Vineet Singh (co-supervised with Amitabha Sanyal ) |
An Abstraction based Approach Towards Translation Validation |
| B. Tech. | Divya Raghunathan (co-supervised with Akshay S. ) |
Knowledge Compilation for Boolean Functional Synthesis |
| Jatin Arora (co-supervised with Akshay S. ) |
Knowledge Compilation for Boolean Functional Synthesis |
| B. Tech. | Shubham Goel (co-supervised with Akshay S. ) |
Boolean Functional Synthesis |
| Sumith Kulal (co-supervised with Akshay S. ) |
Boolean Functional Synthesis |
| Ph. D. | Ajith K. John | Scalable Quantifier Elimination Techniques for Formal Verification |
| Kuldeep S. Meel (co-supervised with Moshe Y. Vardi) |
Constrained Counting and Sampling: Bridging the Gap between Theory and Practice | |
| M.Tech. | Anubhav Sharma (co-supervised with Amitabha Sanyal ) |
An Abstraction based Approach Towards Translation Validation |
| Anjan Chowdhury (co-supervised with Akshay S.) |
Formal Models and Methods in Biological Systems |
| Ph. D. | Abhisekh Sankaran (co-supervised with Bharat Adsul) |
A Generalization of the Łoś-Tarski
Preservation Theorem IIT Bombay Excellence in Thesis (CSE) Award 2017 |
| M. Tech. | Rakesh Mistry | Enginering SMT Solvers for Some Problems in the Theory
of Bit-Vectors Department of CSE Best M.Tech. Thesis Award 2016 |
| M. Tech. | Harshit Pande (co-supervised with Akshay S. ) |
A Constraint Programming Approach to Modeling Gene-Regulatory Networks |
| B. Tech. | Ankush Das (co-supervised with Akshay S. ) |
Termination of Initialized Integer Linear Loop Programs |
| M. Tech. | Dinesh Chhatani | Disjunctive Decomposition of Implicit State Transition Graphs |
| M. Tech. | Rajkumar Gajavelly | An Approach to Word-level Symbolic Trajectory Evaluation |
| B. Tech. | Pritish Kamath | Musings in Logic and Model Theory |
| Vivek Madan | Preservation under Substructures modulo Bounded Cores |
| Ph.D. | Hrishikesh S. Karmarkar | Improved Constructions for Complementation, Disambiguation and Disambiguation of ω-automata |
| M. Tech. | Vaibhav Kulkarni | Studying ∀* ∃* for Finite and Co-finite Spectrum |
| Dual Degree | Rahul Srinivasan | Model Generating Satisfiability Solvers for Quantified Boolean Formulae |
| B. Tech. | Rohit Singh | Termination of Intialized Rational Linear Programs |
| Nisarg Shah | New Procedures for QBF Solving | |
| Manas Joglekar | On Disambiguation of Buchi Automata |
| Ph.D. | Bhargav S. Gulavani | On Improving the Precision of Static Program Analysis IIT Bombay Excellence in Thesis (CSE) Award |
| M. Tech. | Ashutosh N. Kulkarni | Design and Implementation of a RTL Symbolic Simulator |
| Sourabh Moitra | Techniques for Simplifying Symbolic Expressions in Symbolic Simulation based Formal Verification Tools | |
| Dual Degree | Parakram Majumdar | Existential Quantification in Boolean Logic using Factor Graphs |
| Ph.D. | Joycee Mekie (co-supervised with Dinesh K. Sharma ) |
Interfacing Solutions for Globally Asynchronous Locally Synchronous (GALS) Systems |
| M. Tech. | Annervaz K.M. | Approximate Image Computation in Conjunctively Partitioned State Transition Systems with Small Support Sets |
| Jaideep Ramachandran | Disjunctive Decomposition of Circuits for Facilitating Bounded Search of Large State Spaces | |
| B. Tech. | Aaditya Ramdas | Termination of Linear Programs |
| M. Tech. | Kaustubh Nimkar | SMT Solving with Fixpoint Constraints on Bit-vectors |
| Nachiket Vaidya | Developing a Symbolic Simulator for VHDL for use in Verifying Hierarchical Hardware Systems | |
| B. Tech. | Sangram Raje | Extending SMT Solvers for Fixpoint Constraints |
| M. Tech. | Kanika Nema | Parameterised Merging of Heap Abstractions |
| Sasidhar Sunkari | Word-level Symbolic Simulation of Microprocessors | |
| Dual Degree | Sudeep Juvekar | Efficient Approximate Reachability of State Transition Systems with Local Interactions |
| B. Tech. | Aditya Parameswaran | Deciding Termination of Linear Programs |
| Ankur Taly | Approximate Symbolic Reachability of Timed Digital Circuits | |
| Ayush Choure | A Study of Boolean Quantification using Incremental SAT Solving |
| M.Tech. | Saurabh Joshi | Symbolic Model Checking of Large Sequential Circuits |
| Dual Degree | Abhisekh Sankaran | Reachability Analysis in Graph Transformation Systems |
| B.Tech. | Varun Kanade | Guided Symbolic Reachability using Partitioning |
| Pradeep Kanade | Hierarchical Symbolic Timing Analysis of Timed Circuits |
| M.Tech. | Bhargav Gulavani | Symbolic Timing Verification and Analysis |
| Rajeev A.C. | Approximate Verification of Timed Systems | |
| Dual Degree | Dina Thomas | Reachability Analysis of Sequential Circuits: Encoding and Analysis Techniques |
| Shweta Gehlot | Verification of Systems with Data and Control with Symbolic Simulation and Validity Checking | |
| B.Tech. | Vibhor Rastogi | Techniques in Symbolic Model Checking |
| Supriya Garg | Reasoning about Timing in GALS Systems |
| M.Tech./M.S. | Babita Sharma | Bounded Validity Checking of Interval Duration Logic |
| M.S. Maymon | From State Transition Diagrams to CTL Formulae: An Aid for Property Specification | |
| B.Tech. | Vaibhav Mehta | Techniques in Symbolic Model Checking |
| Rajat Dhariwal | Approximate Verification of Timed Automata |
| M.Tech. | Ashutosh Trivedi | Decomposition-based Symbolic Reachability Analysis |
| Shivani Bhatia | Modeling, Simulation and Formal Analysis of Real-Time Client-Server Algorithms | |
| Lakshmi Narasu M.P. | Semi-automatic Generation of Properties for Verification | |
| Nitin S. Kulkarni | Approximate Verification of Timed Automata (discontinued without completing) | |
| B.Tech. | Himanshu Jain | Decomposition-based Symbolic Model Checking for Liveness properties |
| Geet Bhanawat | Clock Elimination in Timed Automata by Symbolic DBMs and Constraint Solving | |
| Jaisingh Solanki | Complexity Analysis of a Subproblem in Symbolic Model Checking | |
| Abhay Golecha | Timing Analysis of Asynchronous Circuits |
| M.Tech. | Nitin Raut | Timing Analysis of Transistor Level Asynchronous Circuits |
| Dual Degree | Apoorv Gupta | Decomposition based Approaches for Synthesizing Asynchronous Circuits from Signal Transition Graphs |
| B.Tech. | Arvind Soni | Symbolic Reachability Analysis by Model Decomposition |
| Mithun Arora | Approximating Timed Automata by Clock Elimination | |
| Sumit Jain | Timing Analysis of Transistor Level Asynchronous Circuits |
| B.Tech. | Rohan Angrish | Probabilistic Time Separation of Events Analysis |