当前位置:首页  开放交流  学术讲座

学术讲座:Automated Verification via Separation Logic

时间:2015-03-02浏览:0

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.  

  

学术报告时间:2015310日上午1000

学术报告地点:博学楼(一教)701