Formal verification has the potential to play a central role in the development of interactive safety-critical systems by providing rigorous guarantees about system behavior. However, the effective use of verification results remains a challenge in practice, particularly when these results must be interpreted by designers and domain experts who will not be formal methods specialists. This paper explores the use of Large Language Models (LLMs) to generate natural language explanations of counterexamples produced by model checking. More specifically, we present a study evaluating how different LLMs handle counterexamples produced from a range of formal models. Our focus is on the potential of LLMs to serve as mediators between formal verification tools and the multidisciplinary teams that design, develop, and validate interactive systems. The goal is to bridge the gap between formal outputs and human understanding. By examining the limitations and opportunities of the use of LLMs, we contribute to a broader discussion on integrating AI technologies into the engineering of trustworthy interactive systems.

 

@InCollection{MoreiraC:2025b,
 author = {E. Moreira and J.C. Campos},
 title = {On the use of LLMs to explain model checking counterexamples},
 booktitle = {Engineering Interactive Computer Systems},
 publisher = {Springer},
 series = {Lecture Notes in Computer Science},
 volume = {16511},
 year = {2026},
 pages = {86-104},
 doi = {10.1007/978-3-032-26051-2_8},
 abstract = {Formal verification has the potential to play a central role in the development of interactive safety-critical systems by providing rigorous guarantees about system behavior. However, the effective use of verification results remains a challenge in practice, particularly when these results must be interpreted by designers and domain experts who will not be formal methods specialists. This paper explores the use of Large Language Models (LLMs) to generate natural language explanations of counterexamples produced by model checking. More specifically, we present a study evaluating how different LLMs handle counterexamples produced from a range of formal models. Our focus is on the potential of LLMs to serve as mediators between formal verification tools and the multidisciplinary teams that design, develop, and validate interactive systems. The goal is to bridge the gap between formal outputs and human understanding. By examining the limitations and opportunities of the use of LLMs, we contribute to a broader discussion on integrating AI technologies into the engineering of trustworthy interactive systems.}
}

Generated by mkBiblio 2.6.28