Generative AI for Formal Verification

About the Project

This project tests the limitations of generative AI (genAI) in formal verification. LLMS is increasing its capability in solving hard problems in science and the real world. For instance, LLMs are proven to be as competitive as human algorithms in predicting logical validity, satisfiability and program termination in formal verification. Moving beyond theoretically hard testing, this project focuses on testing practically hard challenges: we aim to study how good LLMs can predict formal specifications for missing source code (aka unknown functions) in software production.

This genAI-based technique is an analogy of specification inference techniques (such as bi-abduction), which can generate a logical summary for a given source code. Since deploying software with a third-party unknown function is inevitable, a successful genAI-based technique for unknown functions will achieve a great impact; it significantly enhances the formal proofs of both the presence and absence of bugs in the software codebase.

This project will also involve the iterative development of robust software prototypes and their experimental evaluation against the state-of-the-art.

The PhD will provide training in programming principles, logic, and formal verification.

Essential: Degree in Computer Science, Mathematics, or related; strong programming skills; and a proven aptitude for theoretical work.

Desirable: Experience with formal methods (e.g., Hoare logic, separation logic, incorrectness logic, bi-abduction, Coq, Lean), and Generative AI. Ideal candidates should have a Master’s degree with a solid technical background and interest in programming languages and logical methods in computer science.

Please contact the advisor (Dr Quang Loc Le) directly with questions or if interested. Applications from underrepresented groups in computer science are strongly encouraged.