报告题目:Decision procedures for separation logic with inductive definitions
主讲人：吴志林 中科院软件所 计算机国家重点实验室
Separation logic is an extension of Hoare logic, proposed by Peter O’Hearn and John C. Reynolds around 2000, to verify programs manipulating dynamic data structures (aka heaps). Since its introduction, separation logic has become a very popular approach for the analysis and verification of heap-manipulating programs, and many tools have been developed. A notable one is the INFER tool, which has been bought by Facebook and is now actively used in its development process. Because the decision problems of separation logic are undecidable in general, many tools based on separation logic only provide heuristics or incomplete decision procedures for separation logic. Nevertheless, complete decision procedures are desirable to increase the precision and usability of these tools. In this talk, I will report our recent work on complete decision procedures for separation logic with inductive definitions (SLID). We focus on fragments of SLID that are capable of specifying both the shape properties (e.g. binary trees) and data-size constraints (e.g. sortedness and self-balancedness) of dynamic data structures.
Zhilin Wu is an associate research professor in State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. His research interests include program analysis and verification, computational logic, and automata theory. He obtained Ph.D. degree in 2007 from State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences. His research results have been published in famous international conferences e.g. LICS, CAV, IJCAR, CONCUR, IJCAI, AAAI, and international journals e.g. Information and computation and Theoretical Computer Science.More information can be found in his homepage, http://lcs.ios.ac.cn/~wuzl.