Automated Verification via Separation Logic

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.

Short bio

Cristina David is a PhD student at the National University of Singapore, under the supervision of Prof Chin Wei-Ngan. She started her graduate studies in 2006 after obtaining her BSc from Politehnica, University of Bucharest (Romania). Her research focuses on automated program verification. More specifically, she has been working on verification of heap-manipulating programs, proving structural and quantitative properties of data structures, and verification of object oriented programs.

Resources

• talk slide