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
PCP Theorem and Hardness of Approximation [slides] (Seminar Presentation)
Well Structured Transition Systems [slides] (Seminar Presentation)
Topics in Probabilistic Verification [report] (Research Project)
* Also see Courses for a brief description of course projects.
Working on developing efficient verification techniques for concurrent programs in the paramterized setting (where the number of processes is arbitrary).
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 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.
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.
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.