Statement of Purpose Essay - Institute of Science and Technology Austria

What I Like to Research My research interests lie in the field of formal methods in software and systems analysis, from static verification to run-time monitoring. I particularly like to work on projects where I am involved in the (re-)design or analysis of a software system using a well-defined and versatile formal model. Developing such a model can result in proving strong properties about a system (such as being correct by construction), which in turn greatly helps in reasoning about its behavior. In such settings, defining a versatile model can call for a new language (or tool), particularly designed to support what is required for fully describing the model, and be intuitive enough for doing so. Solving challenges of this nature in a project is very interesting to me; I find it rewarding to design a system with strong guarantees about its behavior, or a language that makes specifying such a system easier. More toward the run-time end of the spectrum, I also enjoy working on run-time verification and monitoring of software systems. Run-time monitoring is particularly challenging as it limits our knowledge to a single, finite run of the system, and not all properties can be monitored with this single run. Sometimes, conjoining the original property with a just assumption about the system structure can make more properties monitorable. In the case of quantitative monitoring, statistical approaches, such as modeling with random variables and using confidence bounds, can come to our help. The run-time verifier also needs to be very efficient, and incur low overhead to the existing configuration of systems. This again rules out many exact solutions which are time- or memory-intensive. I enjoy spending time on problems in this direction, partly for the variety of tools and ideas required to design a monitoring mechanism. What Motivates Me For Such Research For me, the ability to reason confidently about the behavior of a complex program is very exciting. That is why, in my undergraduate years, I got very eager to learn topics on formal reasoning about programs and systems. I particularly like to see the output of a research project materialized and put to use in the real world, as it can help in building safe and dependable real-world systems. I also enjoy the implementation phase of research work. Compiling ideas and models to programs introduces new problems that require good knowledge of hardware-imposed limits and software design practices. Providing good solutions to such problems can significantly change the degree of efficiency and maintainability of the final developed tool. My Previous Research Experiences My first research experience was working with Dr. Hossein Hojjat and his graduate student Amir Hossein Seyhani. In this work, we studied a notion of causality, primarily introduced by Halpern and Pearl, and applied this notion to the context of a concurrent system, modeled by a transition system or event structure. Applying a robust framework of causality to real systems can help in analyzing the root causes of failure in complex settings, and building systems that are more secure and less error-prone. In this project, I implemented event structure composition and translation to a causal model in a prototype tool for defining and verifying causes in event structures. I also translated some of the classic causality problems (priorly studied by Halpern and Pearl), as well as simple computer network configurations, into our desired models. I am currently working on optimizing our cause-verifier module, which checks whether a given cause, accompanied by a given witness, can satisfy the Halpern-Pearl causality criteria. For this problem, I am using ideas from previous publications in this direction (such as search space reduction and special-case solutions). I continued research in formal methods by taking part in the summer internship (ISTernship) program at the Institute of Science and Technology (IST) Austria. Here, I joined Prof. Thomas Henzinger’s group and collaborated with two group members. We designed run-time monitors for verifying fairness properties on black-box systems. In this setting, we assumed the underlying system is a Markov chain, and our monitors provide a confidence level for the satisfaction of a fairness property, given an error threshold. We used both the frequentist and Bayesian statistical approaches in our designs. As a means of comparison, we relied on two well-known problems of fairness; concretely, we studied the bank lending and college admission problems, with equal opportunities and social burden as our fairness metrics, respectively. During this internship, I developed a Rust codebase to define and examine our monitors. In addition to that, I mapped the mentioned classic problems to Markov chains, and helped with developing our theories; more specifically, I discovered that Bayesian monitoring is computationally cheap (and can be reduced from evaluating factorial expressions to updating counters) when our fairness expression is in polynomial form. I also showed monitoring fixed-size regular expressions is directly feasible with our existing monitors. Our (current) results for this project are now submitted to TACAS 2023. Why I am Applying to ISTA The academic expertise of ISTA faculty members, along with a community of ambitious students, provides a great environment for me to pursue my research as a Ph.D. student. In particular, I think my interests will align well with Prof. Thomas Henzinger’s course of research. His recent work on monitoring techniques and run-time verification has caught my interest. Furthermore, the work of Prof. Krishnendu Chatterjee on static analysis of programs and automata theory, such as the paper Proving Non-termination by Program Reversal, has caught my attention, and working as a Ph.D. student under his supervision is a path I like to take for my future.