Artificial Intelligence (AI) assisted software solutions have made substantial inroads in critical aspects of modern existence where they routinely make safety-, socio-, and legal- critical decision with certainty and swift. Instances of such AI-assisted decisions include: self-driving cars deciding to stop, implantable pacemakers deciding to pace, or the COMPAS (Correctional Offender Management Profiling for Alternative Sanctions) software deciding if individuals are prone to reoffend. These AI-assisted software are data-driven: they adapt their behavior based experiences in the form of data: be it the expertly curated data in supervised learning, surprising patterns hidden in raw data in unsupervised learning, or the self-generated data guided by expertly designed reward signals in reinforcement learning. The focus of my research is on enabling rigorous system engineering of data-driven system towards improved safety, privacy, fairness, and accountability.

While formal methods for rigorous system engineering provide principles, processes, and practices for traditional systems development, data-driven systems---due to their statistical, inductive, and adaptive nature---demand a paradigm shift. My research seeks to understand and to redefine the role of formal methods in data-driven system development. While I continue to leverage my expertise in analyzing functional requirements including safety and privacy, I am actively exploring the applications of formal methods in analyzing legal and societal implications of data-driven software systems. Some notable examples from my current research include:

• the role of formal requirements in reinforcement learning ,
• the use of automatic testing and debugging in fairness-aware configuration of machine learning libraries, and
• the role of formal specifications in expressing correctness requirements for the tax-preparation software.