AI RESEARCH
Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verification
arXiv CS.AI
•
ArXi:2410.19940v4 Announce Type: replace-cross Formal verification using proof assistants, such as Coq, is an effective way of improving software quality, but requires significant effort and expertise. Machine learning can automatically synthesize proofs, but such tools are able to prove only a fraction of desired software properties. We