Upcoming Q-Activate Event

The integration of Large Language Models (LLMs) into formal verification represents a transformative opportunity to address longstanding challenges in software correctness assurance. This presentation explores the motivations driving this convergence, examines the technical challenges that need to be faced, and presents novel approaches for combining LLMs with traditional verification methods at the semantic level.

We begin by discussing the compelling motivations for applying LLMs to formal verification, including enhanced automation, knowledge transfer across domains, and improved accessibility of formal methods. Simultaneously, we address the significant challenges posed by LLMs' inherent limitations in logical reasoning, consistency guarantees, and the critical need for trustworthy verification results.

The presentation will contrast Bounded Model Checking (BMC) and Interactive Theorem Proving (ITP) paradigms, highlighting their respective strengths and limitations. While BMC excels in finite state exploration, it suffers from fundamental bounded verification constraints. ITP enables unbounded proofs but requires more extensive expertise and manual intervention, presenting challenges for LLM integration.

Drawing from recent research contributions, I will present a comprehensive overview of my requirements engineering conference paper "Supporting Software Formal Verification with Large Language Models: An Experimental Study" that introduces a novel methodology combining LLMs with BMC for automated requirements verification. Key insights will be shared regarding effective prompt engineering strategies and handling verification uncertainty. The presentation will also discuss the practical difficulties encountered and lessons learned during implementation.

Finally, we explore cutting-edge approaches for leveraging LLMs to transcend BMC's bounded verification limitations. This includes automated generation and optimization of loop invariants, strategic use of contract specifications to guide verification processes, and the potential for achieving unbounded formal proofs through intelligent LLM-assisted reasoning. These hybrid approaches promise to revolutionize formal verification by providing more automated, scalable, and accessible verification solutions.

As a second-year PhD student, I aim to share some preliminary findings and perspectives from my ongoing research, while looking forward to learning from the valuable insights and feedback of the community. This presentation represents an opportunity for collaborative discussion on future directions in this rapidly evolving field, targeting researchers and practitioners interested in the intersection of AI and formal methods.