Juan Zhai

Juan’s long-term research goal is to advance software engineering by developing innovative techniques for building high-quality software systems. Her work addresses a fundamental challenge in software development: real-world implementations are often difficult to verify against their intended behavior. To bridge this gap, she creates automated methods for inferring and enforcing behavioral specifications, enabling both developers and systems to reason more effectively about various aspects of program behavior, including correctness, fairness, robustness, and safety. These methods also support the detection, diagnosis, and repair of behavioral violations in both traditional and AI-powered systems.

Her research investigates two main directions: automatically inferring and maintaining software behavior specifications, ranging from formal, machine-executable representations to informal, natural language descriptions; and automatically detecting and repairing defects through behavioral reasoning. Her broader vision is to integrate these efforts into an automated framework where specifications serve as the foundation for end-to-end assurance, allowing systems to be validated, repaired, and audited continuously as they evolve in complex, data-driven, and dynamic environments.