Title: Automated Verification via Separation Logic

Speaker: Dr. Shengchao Qin

　　　Teesside University, Middlesbrough, UK

Time: 3:00pm, Friday, Nov. 12

Venue: Lecture room, Lab for Computer Science, Level 3 Building #5, Institute of Software, CAS

Abstract: 

Despite their popularity and importance, pointer-based programs remain a major challenge for program verification. In recent years, separation logic has emerged as a contender for formal reasoning of pointer-based programs. Recent works have focused on specialized provers that are mostly based on fixed sets of predicates. In our work, we propose an automated verification system (Hip/Sleek) for ensuring the safety of pointer-based programs, where specifications handled are concise, precise and expressive. Our approach uses user-definable predicates to allow programmers to describe a wide range of data structures with their associated shape, size and bag (multi-set) properties. To support automatic verification, we design a new entailment checking procedure that can handle well-founded predicates (that may be recursively defined) using unfold/fold reasoning. We have proven the soundness and termination of our verification system and built a prototype system to demonstrate the viability of our approach.

In this talk, I’ll first introduce the Hip/Sleek verification system (mainly developed by my collaborators in NUS). I’ll then move on to a more recent piece of work (to appear in ICFEM2010) on loop invariant synthesis in a combined separation and numerical domain.

Short Bio:

Shengchao Qin obtained his BSc (1997) and Ph.D (2002) from Peking University. In July 2002, he joined National University of Singapore for a Research Fellowship under the Singapore-MIT Alliance, and then took up a lectureship in Durham University in UK in January 2005. He has very recently moved to Teesside University for a Readership. Shengchao’s research interests mainly lie in formal methods and programming languages, with a recent focus on automated verification of pointer-based programs. He has been the principal investigator of two EPSRC projects in UK. More information can be found at his personal webpage http://www.scm.tees.ac.uk/s.qin.