Jan 2017 - ongoing
Keywords: Reactive Synthesis, Two-player Games, Symbolic Algorithms
GenSys paper | GenSys-LTL paper | GenSys Video | GitHub
Joint work with Deepak D'Souza and Raghavan Komondoor, Indian Institute of Science, Bangalore
The first work deals with the synthesis of maximal controllers for logical LTL games with safety specifications; this work was accepted in the tool demonstrations track at ESEC/ FSE 2021.
The second work extends the above work to handle general LTL specifications; this work was accepted in the research papers track at ASE 2023.
Sep 2019 - March 2020
Keywords: Reactive Synthesis, Control Theory, Synthesis for Continuous Dynamical Systems
arXiv | Video | RESCOT Tool | Poster
Joint work with Max Planck Institute for Software Systems, Kaiserslautern, Germany.
This work has been accepted for poster presentation at the 23rd ACM International Conference on Hybrid Systems: Computation and Control (HSCC), 2020.
This work has been accepted for full paper presentation at the 59th Conference on Decision and Control (CDC), 2020
Aug 2018 - Dec 2018
Platform: Java; Analysis tool: IBM WALA
In this project, we implement a Null Dereference analysis which uses the Iterativeapproach for interprocedural points to analysis. In the iterative approach, weessentially compute the summary functions for each procedure iteratively. We de-couple the propagation of function rows and maintain a table of values representingthe summary function for each program point in a procedure.
Aug 2017 - Dec 2017
Platform: Java; Analysis tool: IBM WALA
Flow-sensitive pointer analysis computes for each program point what memorylocations pointer expressions may refer to. In this project, we use Kildall’s algorithmover a suitable Abstract Interpretation framework for computing this points-toinformation at every point.
Flow-insensitive pointer analysis computes what memory locations pointer ex-pressions may refer to, at any time in program execution. In this project, weuse Anderson’s algorithm over a suitable Abstract Interpretation framework forcomputing this points-to information at every point.
Total ordering atomic broadcast protocol using token ring
March 2017 - April 2017
Technologies used: C
August 2016 - December 2016
Platform: Java; Analysis Tool: Soot Framework; Solver: Z3 by Microsoft
In this project, a Record and Replay tool based on the PLDI’ 13 paper ’CLAP:Recording Local Executions to Reproduce Concurrency Failures’ was implemented.Record and Replay tools are fundamental to dynamic program analysis.
More specifically, concurrency bugs are reproduced as follows. In the first step,thread local execution paths are logged at runtime. This step uses the BallLarus profiling technique (Efficient Path Profiling, MICRO’ 96) to record the pathconstraints and program order constraints. In the second step, we also add interthread constraints and feed it to the constraint solver Z3 to get a global schedulethat reproduces the bug. This step is computed offline.
Feb 2015 - May 2015
Technologies used: Craft CMS, Virtual Box using Laravel Homestead, Git, Grunt, Sass
Worked on a four month project for Aranca, a leading provider of customized investment research, business research, intellectual property research and valuation services to global clients. My work involved designing and developing the front end architecture. The highlight of this project was working with Web Components on the front end. We had to design modules which could be placed anywhere on the website without breaking the site.
September 2011 - May 2012
Technology used: MATLAB
My final year augmented reality project based on color detection, image processing and sound processing techniques.
