Garvit Juniwal

Garvit Juniwal 

Masters in Science
Electrical Engineering and Computer Sciences
UC Berkeley
Advisor: Prof. Sanjit A. Seshia

View Garvit Juniwal's profile on LinkedIn

About        Thesis        Publications        Tools        Research        CV(in pdf)

About Me

I graduated in 2014 after finishing Masters degree.

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




CyberSim and CPSGrader (Master's thesis project)

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 (software)

Bio Model Analyzer (Internship project at Microsoft Research Cambridge)

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


Symbolic SyGuS Solver

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.

Details    (github)

Other Research

For detailed reports/presentations, please contact me.