My interests lie in the use of formal techniques to model, verify and synthesize safe computing systems. I have worked in applications spanning biological models, cyber-physical systems, and networks. 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.
Keywords: Formal Methods, Automatic Grading, Robotics, Cyber-Physical Systems, Program Synthesis, Computational Biology, Network Verification
Nikolaj Bjorner, Garvit Juniwal, Sanjit A. Seshia, George Varghese, and Ratul Mahajan. ddNF: An Efficient Data Structure for Header Spaces. In Proceedings of the Haifa Verification Conference (HVC), November 2016. Best Paper Award.
Garvit Juniwal, Sakshi Jain, Alexandre Donzé, and Sanjit A. Seshia. Clustering-Based Active Learning for CPSGrader. In Proceedings of the Second ACM Conference on Learning @ Scale (L@S), March 2015.
Jyotirmoy Deshmukh, Alexandre Donzé, Shromona Ghosh, Xiaoqing in, Garvit Juniwal, and Sanjit A. Seshia. Robust Online Monitoring of Signal Temporal Logic. In Proceedings of the International Conference on Runtime Verification (RV), September 2015. Best Paper Award.
Garvit Juniwal, Alexandre Donzé, Jeff C. Jensen, Sanjit A. Seshia. CPSGrader: Synthesizing Temporal Logic Testers for Auto-Grading an Embedded Systems Laboratory. In Proceedings of the 14th International Conference on Embedded Software (EMSOFT), October 2014.
Details Download: pdf
Byron Cook, Jasmin Fisher, Benjamin A. Hall, Samin Ishtiaq, Garvit Juniwal, Nir Piterman. Finding Instability in Biological Models. In Proceedings of the 26th International Conference on Computer-Aided Verification (CAV), July 2014.
Details Download: pdf Talk: ppt
Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, and Abhishek Udupa. Syntax-Guided Synthesis. In Proceedings of the IEEE International Conference on Formal Methods in Computer-Aided Design (FMCAD), pp. 1-17, October 2013.
Details Download: pdf
Developed an automatic grading cum feedback generation component (auto-grader or CPSGrader) for the simulation driven virtual robotics laboratory (CyberSim) used in the online Cyber-Physical Systems course EECS 149.1x offered on edX. This is the first online course to use a virtual laboratory and the first deployed auto-grader that uses formal verification. CPSGrader uses Signal Temporal Logic based test benches to monitor simulation traces of student solutions. Each test bench serves as a classifier to detect presence of a particular kind of fault and we automatically learn/synthesize the classification boundaries using a library of previously known correct and faulty solutions. The robotics simulator is written in LabVIEW, the auto-grader is an independent library written in C++ that plugs into the simulator, and the test bench synthesis is done in MATLAB using the Breach toolbox. A survey conducted at the end of the course shows that 86% of students find the feedback from the auto-grader crucial in completing the lab exercises.
Details cpsgrader.org (software)
Bio Model Analyzer is an online tool that allows biologists to create and analyze stability properties of protein signaling networks. As a contributor to the tool, developed a stability-proving/instability- finding back-end that scales to models with few hundred proteins. The algorithm tries to find cyclic instability using interval abstraction of the transition system in a divide/conquer fashion. Implemented primarily in F#.
Developed the symbolic solver for Syntax-Guided Synthesis competition. The solver inductively synthesizes a program directly from a high-level specification working through counter-examples. It uses the SMT solver Z3 both for synthesis (learning program from input-output examples) and verification (finding counter-examples) phases. The solver is primarily written in Python using Z3's Python API. This was publicly released as one of the three baseline solvers.
Quantitative Network Verification July 2014 - date
Microsoft Research, Silicon Valley Campus Prof. George Varghese, Dr. Nikolaj Bjorner, Dr. Ratul Mahajan, Prof. Sanjit A. Seshia
Developing efficient data structures and abstraction mechanisms for static verification of networks with large packet headers. By encoding to a disjoint normal form using difference of ternary bit vectors, we transform a large graph over header spaces to a smaller equivalent graph which we use for verification of quantitative properties such as those involving bandwidth, rate limits and latency. We have been able to successfully run on Azure data center networks, which would assist network operators to find high cost bugs before they manifest. The abstraction and quantity propagation engines (implemented in C#) are heavily optimized to be scalable and high performing.
Clustering-Based Active Learning for CPSGrader   Spring 2014
CS 281A, UC Berkeley Sakshi Jain, Prof. Michael Jordan
CPSGrader (the auto-grader used in the online Cyber-Physical Systems course EECS 149.1x) learns a fault classifier using a few examples of correct and faulty student solutions as training data. Unlabeled data is abundant but manually labeling as faulty/non-faulty is tedious. We developed an active learning algorithm to choose the new data points to obtain labels for. The data points in our case are multi-dimensional time series obtained from the physics-based robotics simulator CyberSim. We cluster the data using density based scanning (DBSCAN) with dynamic time warping (DTW) distance as the dissimilarity measure. Active learning enables us to achieve same accuracy levels for the classifier using fewer training examples as compared to random data point selection. DTW computation is implemented in R and the clustering algorithm in Python.
Reactive Synthesis using Sketching Fall 2012
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 the moves on a grid avoiding obstacle and reaches final destination.
Decidability of Emptiness Checking in various Alternating Timed Automata and Connections to Timed Logics (B.Tech Thesis) 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 expressive 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
Goal is to automatically infer labels on parts of a software so that it probabilistically satifies some path safety property. In web applications, it is required that every source to sink path has a sanitizer on it. We automatically label parts of the program as source/sink/sanitizer to enable checking this requirement. We model the program-property product as a Markov chain and analyze its structure to reason about steady state error probabilities. Implemented in C# 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
Designed an algorithm for automated synthesis of maximally permissive deadlock prevention control for systems composed of interacting state machines. Implemented in Java by reduction to Integer Linear Programming using ideas from similar work for Petri Nets.
For detailed reports/presentations, please contact me.