Guruprerana Shabadi

...you can call me Guru!

Master's student in Computer Science at École Polytechnique & Research Intern at IMDEA Software Institute, Madrid

CV

I am currently a candidate in the Parisian Masters of Research in Computer Science (MPRI) program at École Polytechnique. I previously graduated from École Polytechnique with a bachelor's degree in mathematics and computer science. My set of core research interests is spanned by the following grammar:

$\Phi \Coloneqq \hspace{0.2cm} \varphi \hspace{0.2cm} \textit{ for } \hspace{0.2cm} \varphi \hspace{0.2cm}$ $\\ \varphi \Coloneqq \text{ program synthesis } \mid \text{ verification } \mid \text{ AI } \mid \text{ automation }$

As a result, I am also interested in all topics that play a role in these domains including (but not restricted to) logic, model checking, reinforcement learning, game theory, control, cyber-physical systems, PL, NLP etc.

I am currently an intern at IMDEA Software Institute, Madrid working with Alessio Mansutti on arithmetic logic. Previously, I worked with Nathanaël Fijalkow on worked on synthesizing programmatic policies for (a small subset of) markov decision processes (MDPs) starting from programmatic representations of these MDPs (visualized by some cool animations). Before that, I worked with Caterina Urban on building a abstract interpretation based tool to verify data science Jupyter notebooks (SOAP'23). And I started my journey in the world of formal methods research working with Sergio Mover on handling communication delays arising in cyber-physical systems. More info on all these works below! A cheesy long term goal of mine is to build a world in which autonomous systems are both omnipresent and guaranteed to be safe, and where automation drives the march towards sustainable development.

When I am not verifying programs/autonomous systems around me, I dabble in software development and I am currently working with a team of 4 brilliant innovators on building Anemone! Lastly, education is something I am deeply passionate about and a long term goal of mine is to work on improving computer science education and outreach.

What's up with me!

Publications

Research Experience

Bachelor thesis: Static analysis of data science software (January 2022 - April 2022)

Worked with Caterina Urban at the ANTIQUE team of ENS, Paris on the design of abstractions to facilitate static analysis of Jupyter notebooks used for data science.

[Paper][Slides][Thesis][Abstract]

Abstract. Availability of data at extensive scales has led to the adoption of data-driven decision making practices in several domains including the likes of medicine, finance, and public policy. Consequently, ensuring correctness and fairness of analyses drawn from data science programs is critical and presents a challenging verification task. Errors in data processing code often go unnoticed since they do not throw errors, and can lead to unsound conclusions being drawn from data. We propose an abstract interpretation based static analysis tool as a first step towards analysing data science programs. To this end, we construct a novel abstract domain to track data transformations which we exploit towards the task of shape inference of input data. Our tool is capable of automatically inferring the constraints and assumptions placed by a program on the input data. This can be further used towards achieving bigger objectives like input data usage analysis, data provenance, and the detection of bias or skew introduced in the data by a program.

Accounting for communication delays in a hybrid system (June 2021 - December 2021)

Worked with Sergio Mover with the Cosynus team at LIX (computer science department at Ecole Polytechnique) on handling communication delays which arise when there are multiple hybrid systems interacting with each other.

[Talk][Slides][Report][Abstract]

Abstract. Cyber-physical systems use communication protocols to gather information on their environments in order to react to changes around them. However, in practice these protocols are far from perfect and can have non-negligible delays in relaying state information, i.e., there might be a delay in observing the current value of a state variable. To further motivate the study of these delays, we explore the case study of a collision avoidance protocol with a group of robots navigating in space while avoiding collisions. Here, we cannot ensure that each robot has complete information about the state of the other robots at every instant of time. To model these delays, we revisit the class of hybrid automata called lazy hybrid automata in the continuous, instead of discrete, semantic. Lazy hybrid automata model nondeterministic delays in observing the value of state variables used in invariants and guard conditions. We then discuss the results we have obtained on the expressiveness of some restricted classes of (continuous) lazy hybrid automata by providing their translations into classical hybrid automata.

Software Development

In my free time I like dabbling in software development.

Anemone (October 2020 - Present)

Over the past couple of years, I have been working with 4 other motivated friends (who also happen to be brilliant entrepreneurs) from my university on building Anemone: a socio-professional networking platform tailor-made to the needs of the artistic and cultural industries! I lead the development team at Anemone. Find the app on the French App Store and Play Store. Check out our website!