Automated Verification via Separation Logic Seminars/Workshops

Abstract

In recent years, separation logic has been extensively used for formal reasoning of heap-manipulating programs. Throughout my PhD studies, I have made use of separation logic in designing a prover that can automatically handle user-defined predicates. These predicates allow describing the shape of a wide range of data structures with their associated size and bag properties. The bag properties capture the reachable nodes inside a heap predicate, and consequently, can be used for proving properties about the actual values stored inside a data structure. In the current seminar, I will introduce the use of the aforementioned prover in handling heap-manipulating programs, as well as some extensions for verification of object-oriented and exception-handling programs.