Work Exp.

I am a Senior Software Engineer in Kernel group at Atrenta India Pvt. Ltd. Prior to joining Atrenta, I was associated with Verimag Research Lab in Grenoble as an R&D engineer under the supervision of Dr. Goran Frehse. In past, I also worked at IBM India Labs, Bangalore. I pursued my Masters studies at Indian Institute of Technology Guwahati, where I worked under Dr. Purandar Bhaduri during my masters thesis.

My resume can be found here.

Research Experience
My nterests span Formal Methods, Automata Theory, Logic and Computation.

• Parameter state space refinement
  Parameter Synthesis Problem is to identify sets of parameters for which the system does (does not) reach a given set of states. This safety analysis problem is defined as a reachability problem. Computing the reachable trajectories for the large parameter state space at once can lead to a high over-approximation. The result being sensitive to such parameters, parameter state space is refined into symbolically equivalent states until the safety of the system is decided or a given threshold is arrived. I worked on the algorithm for refinement of parameter state space based on the equivalence of initial states. The task intended to improve speed of reachability analysis of a dynamical system in Breach by use of mex functions.
• Masters Thesis
  Safety verification is defined as a reachability analysis problem. And in hybrid systems, its even more difficult due to their dynamics (discrete and continuous). A lot of research is being performed to find scalable verification methods for these systems due to which various tools have been developed. I evaluated two such tools PHAVer and HSolver, used for safety verication of linear and nonlinear hybrid systems respectively, and concluded about their behaviors in terms of time, memory and decidability. During the evaluation process, we also formulated a strategy to compute linearization error, otherwise difficult to compute, which is incurred during approximation of a nonlinear system by its linear counterpart. At an early stage of my thesis, I also worked in the direction of improving simulation coverage of Simulink/Stateflow models based on the notion of Equivalence of initial states.
• SpaceEx: State Space Explorer
  SpaceEx is a platform to facilitate the safety verification of hybrid and continuous systems. As a part of SpaceEx development team, I have managed various SpaceEx modules ranging from bi-direcitonal transformation between CIF and SX, non-linear function support to the designing of complete automaton library. The tasks involved detailed understanding of CIF and SX grammars, researching over their constructs to find semantic relationships between them. We also made efforts to retain information pertaining to variable scope and automaton template during translation. And, in order to keep the automaton operations complexities within reasonable bounds, we even improvised on few operations such as Union and Intersection based on the fact that only reachable states are relevant in any DFA. The execution time analysis for large inputs emphasizes on the efficacy of our approach that reduces the operation complexity by a numerical factor.

Publications:

1. M. Goyal, “Reachability Analysis of Hybrid Systems: An Experience Report,” in Proc. 3rd International Conference on Computer Modeling and Simulation (ICCMS 2011), Mumbai, Inda: 489-493, IEEE, 2011. (pdf).
2. M. Goyal, G. Frehse, “Translation between CIF and SpaceEx/PHAVer,” Technical Report, MULTIFORM Deliverable D1.3.1, VERIMAG, France: May 2011. (pdf or link @ MULTIFORM)
3. M.Goyal, G. Frehse “Automata Library: A User Guide,” Technical Report, Verimag, France: April 2012.