Click here to flash read.
arXiv:2310.04870v5 Announce Type: replace
Abstract: The demonstrated code-understanding capability of LLMs raises the question of whether they can be used for automated program verification, a task that demands high-level abstract reasoning about program properties that is challenging for verification tools. We propose a general methodology to combine the power of LLMs and automated reasoners for automated program verification. We formally describe this methodology as a set of transition rules and prove its soundness. We instantiate the calculus as a sound automated verification procedure and demonstrate practical improvements on a set of synthetic and competition benchmarks.
Click here to read this post out
ID: 822616; Unique Viewers: 0
Unique Voters: 0
Total Votes: 0
Votes:
Latest Change: April 26, 2024, 7:31 a.m.
Changes:
Dictionaries:
Words:
Spaces:
Views: 7
CC:
No creative common's license
No creative common's license
Comments: