Search

• < Previous
• 1
• Next >

Simulating reachability using first-order logic with applications to verification of linked data structures

This paper shows how to harness existing theorem provers for first-order logic to automatically verify safety properties of imperative programs that perform dynamic storage allocation and destructive updating of pointer-valued structure fields. One of the main obstacles is specifying and proving the&nbsp;[&hellip;]