Garvit Juniwal

First Year PhD candidate Department of Electrical Engineering and Computer Science UC Berkeley Advisor: Professor Sanjit A. Seshia

My research interest is automated synthesis of dependable computing systems. Before Berkeley I spent four wonderful years at IIT Bombay to earn a lot of friends and liberating experiences apart from an undergraduate degree in Computer Science.

Curriculum Vitae

Contact

garvitjuniwal@eecs.berkeley.edu 545S Cory Hall Berkeley CA

Research

• Reactive Synthesis using Sketching Ongoing
  UC Berkeley Prof. Sanjit Seshia, Prof. Ras Bodik
  Formalized the idea of using sketching in reactive controller synthesis. Sketches that we start with are extended FSMs with partially known guards/actions and specifications are in LTL. Synthesis step completes the sketch by bounding number of computation steps of the controller and verification step checks correctness of completed sketch in the unbounded setting. Bound on the number of computation steps is increased until correct program is generated. Analyzed the approach by applying it to examples in the robotic motion planning domain. Could synthesize controller for robot that moves on a grid avoiding obstacle and reaches final destination.

• Decidability of Emptiness Checking in various Alternating Timed Automata and Connections to Timed Logics July,2011-April,2012
  B.Tech project, IIT Bombay Prof. Krishna S(IITB), Prof. Paritosh Pandya(TIFR)
  Decidability for one-clock ATAs is known. Replacing clock with stopwatch enhances expressiveness. We prove that language emptiness for one stopwatch ATA is undecidable. We also show that one variable TPTL can be embedded into one clock ATA. We also define a new class of automata called snoopy ATA and show that it is strictly more ex- pressive than one clock ATA and still has decidable language emptiness. We also show that multiple variable TPTL+F can be embedded into one clock snoopy ATA

• Quantitative Label Inference May-July, 2011
  Microsoft Research, Bangalore Dr. Aditya Nori, Dr. Sriram Rajamani
  The task is to infer unknown labels in a program(Kripke Structure) so that it quantitatively satisfies some path safety property. Solved it by modeling the program-property product as a Markov chain and analysing its structure to reason about stationary probability of reaching the error state. Implemented a tool to infer labels over Kripke Structures for arbitrary path properties using the probabilistic inference library Infer.NET.

• Synthesis of Deadlock Prevention Control for BIP Models May-July, 2010
  Verimag Lab, Grenoble, France Dr. Barbara Jobstmann, Prof. Joseph Sifakis
  Devised a technique to detect and control (by supervision) deadlocks in BIP models. Using ideas from similar work on petri-nets, we were able to reduce the problem of synthesis of maximally permissive (preserving all the useful behavior) deadlock prevention supervisors, to solving a linear program. This was also successfully implemented by using linear solvers.

For detailed reports/presentations, please contact me