Title: Automated Verification via Separation Logic
Speaker: Prof Shengchao Qin（秦胜朝教授）, Teesside University, UK（英国提赛德大学）
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.
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 joined Teesside University as a Reader in June 2010 and became a professor in June 2011. Shengchao’s research interests mainly lie in formal methods and programming languages, with a recent focus on automated verification of pointer-based programs.
学术报告时间：2015年3月10日上午10：00
学术报告地点：博学楼（一教）701