International Symposium On Leveraging Applications of Formal Methods, Verification and Validation • Crete, Greece
Time: Thursday, 31.10
Room: Room 3
Authors: Itay Cohen, Doron Peled
Abstract: The research of Large Language Models (LLMs) has significant ground to cover in the context of formal verification. In this work, we present a methodology that aims to increase the reliability of code synthesized through the use of LLMs. Our approach capitalizes on the intrinsic knowledge embedded within LLMs to achieve a more reliable code synthesis. We specifically illustrate the possibility of teaching model checking and runtime verification (RV) algorithms through our approach. Our experiments demonstrate that LLMs grasp the concept of dynamic programming, allowing them to synthesize code for these verification tasks with minimal guidance.
Paper: Download