Juan Zhai

Formal Specification Synthesis

The fundamental challenge in developing high-quality software is ensuring that its behavior aligns with the intended specifications. At the heart of this challenge is the persistent absence of formal specifications which are precise, unambiguous definitions of expected behavior. Formal specifications are essential not only for traditional activities like debugging, testing, and verification, but also for enabling large language model agents to generate correct and reliable code. Despite their importance, formal specifications remain rare in practice due to the complexity of authoring and maintaining them, especially in fast-evolving, real-world systems.

My research addresses this gap by developing techniques to automatically synthesize formal specifications. Our tool C2S, successfully translates natural language comments into formal specifications, improving test oracle generation, reducing false positives in automated testing, and enhancing static taint analysis. We have also generate LTL formulas for IoT systems from natural language commands, and are now exploring LLM-driven specification synthesis.

Comment Generation and Maintenance

Comments often convey high-level semantic intent, but they are frequently outdated, incomplete, or inconsistent with code. Our research focuses on inferring and maintaining behaviorally accurate comments to support understanding, maintenance, and reasoning.

We developed CPC, a novel software reasoning method that enables bidirectional analysis across comments and code implementation. To keep comments updated as software evolves, we developed LLMCup, a framework that automatically updates comments using large language models with a ranking-based refinement strategy.

Trustworthy AI Analysis and Improvement

As AI-driven software systems increasingly impact critical aspects of society, ensuring their trustworthiness has become both a technical and moral imperative. Our research spans the AI stack, with a focus on improving correctness, robustness, and fairness through practical, scalable tools and techniques.