At the core of my work is the challenge of verifying and validating systems where traditional model-driven approaches may fall short due to oversimplifications and the increasing incorporation of data-driven components. My research addresses these challenges by integrating runtime verification, formal specification languages, and monitoring techniques into the system design process, ensuring more robust assurance in dynamic environments. A key area of my contribution is the analysis of probabilistic programs, where I co-developed tools such as:

• Polar, a framework for automated analysis of probabilistic loops using algebraic reasoning. Polar captures loop semantics through algebraic recurrences and computes closed-form solutions for higher-order moments of variables. It supports probabilistic programs with conditional branches, symbolic parameters, and common distributions, offering both exact and approximate techniques for deriving invariants, parameter sensitivities, and loop behavior.
• Amber, a tool that automates the proof or refutation of (positive) almost-sure termination of probabilistic while-loops. Amber employs martingale-based reasoning and properties of asymptotic bounding functions, allowing it to outperform state-of-the-art tools in analyzing programs with polynomial arithmetic and probabilistic constructs.

• Spatel, SaSTL, and STREL for spatio-temporal properties,
• Signal Convolution Logic (SCL) and Time-Frequency Logic (TFL) for frequency-aware reasoning,
• Open-source tools like Moonlight (spatio-temporal monitoring), CPSDebug (specification mining and failure analysis), and FIM (fault injection and mutant generation for Simulink models).