Shuvendu Lahiri
Talk: AI for Program Specifications
- Date and Time
- February 25, 2025 at 12:30pm
- Location
PLSE Lab (CSE2 253)
Abstract
The correctness of a program is always as good as the specification that is verified. However, writing down precise and formal specifications is non-trivial for mainstream developers. This limits the usage of rigorous testing and verification techniques to improve the quality of code, including those generated by AI. In this talk, I will describe ongoing work on deriving formal specifications from informal source of intent such as natural language docstrings, API documentation and RFC. We describe different ways to formalize the intent as declarative specifications starting with tests, postconditions (in mainstream languages such as Python to verification-aware languages such as Dafny), to data format specifications in 3D language. We formalize metrics to evaluate the quality of various LLM-based techniques using techniques inspired by mutation testing, but with novel encoding requiring mutant generation or invoking formal verifiers. We will describe some early results on fine-tuning models for specification generation. If time permits, we can discuss using AI and symbolic methods to construct provable inductive specifications for program verification in tools such as Frama-C, F* and Verus.
Bio
Dr. Shuvendu Lahiri is a Senior Principal Researcher in the RiSE group at Microsoft Research Redmond. His research interests are in rigorous techniques based on formal methods and machine learning towards reliable software development. He has worked on SMT solvers, formal specification and verification, software testing and other programming tools. He holds a PhD from Carnegie Mellon University and a BTech from IIT Kharagpur. He has served on the program committee of several programming languages, formal methods and software engineering conferences, as well as chaired formal methods conferences. His works has received best/distinguished paper awards from leading formal methods and software engineering conferences, a test-of-time award from ICSE, and lifetime CAV award for SMT solvers, and ACM SIGDA outstanding PhD dissertation award.