My main interests lie in Programming Languages, Verification, and Formal Methods.


  • 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

  • Decidable Toplogies [slides, report] (Seminar Presentation)

  • 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.


Parametrized Verification of Concurrent Programs
With Prof. Krishna S., Prof. Parosh Abdulla and Prof. Faouzi Atig

Working on developing efficient verification techniques for concurrent programs in the paramterized setting (where the number of processes is arbitrary).

Problems on Linear Dynamical Systems [Phase-1 report].
Bachelor’s Thesis under the guidance of Prof. S. Akshay

Systems 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 Figueira

Graph 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 Atig

WMMs define the semantics for memory accesses in multi-threaded 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 Bertrand

We 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.


Email godbole15 at
CSE Dept Mail adwaitg at