Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

LLM-Based Scheme for Synthesis of Formal Verification Algorithms

  • 会议论文

  • 发表日期：

    2025年

查看全文
  • Itay Cohen,
  • Doron Peled

摘要

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.