Automatically Building Machine-Checked Assurance Cases from C Codebases to Requirements

Haokun Li, Zhongyi Wang, Guanyan Li +4

Large language models (LLMs) have shown promise in automating interactive theorem proving, yet verification of real-world C codebases requires more than discharging individual proo…