Learning Assertions to Verify Linked-List Programs

Abstract. C programs that manipulate list-based dynamic data struc-tures remain a challenging target for static verification. In this paper we employ a dynamic analysis to locate and identify data structure op-erations in a program, so as to automatically annotate that program with assertions in separation logic. These annotations comprise candi-date pre/post-conditions and loop invariants suitable to statically verify memory safety with the verification tool VeriFast. By using both text-book and real-world examples on our prototype implementation, we show that the generated assertions are often discharged automatically. Even when this is not the case, candidate invariants are of great help to the verification engineer, significantly reducing the manual verification effort.