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 |