My main interests lie in Programming Languages, Verification, and Formal Methods.
Publication
 Controlling a population^{†}
Nathalie Bertrand, Miheer Dewaskar, Blaise Genest, Hugo Gimbert, Adwait Godbole
Logical Methods in Computer Science, Jul, 2019  Volume 15, Issue 3 [paper] [fun slides]
^{†}Authors’ names in alphabetical order
Seminar Presentations, Reports

PCP Theorem and Hardness of Approximation [slides] (Seminar Presentation)

Well Structured Transition Systems [slides] (Seminar Presentation)

Topics in Probabilistic Verification [report] (Research Project)
Research Projects*
* Also see Courses for a brief description of course projects.
Ongoing
Parametrized Verification of Concurrent Programs
With Prof. Krishna S., Prof. Parosh Abdulla and Prof. Faouzi AtigWorking on developing efficient verification techniques for concurrent programs in the paramterized setting (where the number of processes is arbitrary).
Problems on Linear Dynamical Systems [Phase1 report].
Bachelor’s Thesis under the guidance of Prof. S. AkshaySystems modelled by Markov Decision Processes (MDPs) often have a hard(safety)constraint that needs to be ensured. This constraint may be specified as a containment property for the state probability distribution vector in some polytope (a closed convex space bounded by hyperplanes). The escape problem for Markov Decision Processes (MDPs), asks whether there is an adversarial strategy that takes the state probability vector outside the polytope. We study this problem with the goal of finding a decision procedure.
Graph Database Queries
Research Project under the guidance of Prof. Krishna S., Prof. Wim Martens, and Prof. Diego FigueiraGraph database queries are structural patterns that capture constraints on graph databases and return tuples of satisfying nodes as the answer. We study the boundedness and containment problems in order to characterize complexity and provide algorithms for classes of queries.
Past Projects
Verification of programs under Weak Memory Models (WMMs)
Internship in Summer, 2019 at Uppsala University under the guidance of Prof. Parosh Abdulla and Prof. Faouzi AtigWMMs define the semantics for memory accesses in multithreaded programs. There I worked on theoretical proofs and also developed a model checker for verifying programs. This work is under submission.
Controlling Parallel Asynchronous Agents
Internship in Summer, 2018 at INRIA, Rennes under the guidance of Prof. Blaise Genest and Prof. Nathalie BertrandWe studied a control problem for parallel asynchronous agents which act independently but are controlled uniformly (same action applied to all agents). I worked on bounding the step complexity (number of steps required for synchronization). A paper with these results is a part of LMCS, Volume 15, Issue 3. Here are some slides for an overview of the work.
Thanks to Prof. Nathanael Fijalkow for the Flides template.
Contact
Email godbole15 at gmail.com
CSE Dept Mail adwaitg at cse.iitb.ac.in