Alumni ...


B. Tech. Divya Raghunathan Knowledge Compilation for Boolean Functional Synthesis
Jatin Arora Knowledge Compilation for Boolean Functional Synthesis


B. Tech. Shubham Goel Boolean Functional Synthesis
Sumith Kulal 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


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