Presenter: Zhongyi Wang
Abstract: This talk presents recent research on enhancing the strength and practical applicability of Large Language Model (LLM)-generated formal specifications for C program verification. We discuss two complementary frameworks that address key limitations of prior LLM-based approaches, which often produce specifications lacking semantic depth, verifiability, or sufficient strength for real-world verification tasks.