一作OSDI 2026Oral· Operating Systems & Distributed Systems
Neuro-Symbolic Proof Generation for Scaling Systems Software Verification
Baoding He · Zenan Li · Wei Sun · Yuan Yao · Taolue Chen · Xiaoxing Ma · Zhendong Su
摘要
Formal verification via interactive theorem proving is increasingly used to ensure the correctness of critical systems, yet constructing large proof scripts remains highly manual and limits scalability. Advances in large language models (LLMs), especially in mathematical reasoning, make their int...