最 新 推 荐
  • 此栏目下没有推荐文章
  • 相 关 文 章
    没有相关文章

     您现在的位置: 逻辑与认知研究所 >> 中文版 >> 学术信息 >> 学术讲座预告 >> 正文

    Decision procedures for separation logic with inductive definitions(吴志林,2017/5/2)
    Decision procedures for separation logic with inductive definitions(吴志林,2017/5/2)

     作者:佚名    文章来源:本站原创    点击数:    更新时间:2017/4/28

    更多


    报告题目:Decision procedures for separation logic with inductive definitions

    主讲人:吴志林 中科院软件所 计算机国家重点实验室

    时 间:2017年5月2日(周二)下午15:00-16:30

    地 点:锡昌堂322室

    Abstract:

    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.


    Bio:

    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.


    主办单位:中山大学逻辑与认知研究所


    电话:86-020-84114557 传真:86-020-84110298  电子邮箱:logic@mail.sysu.edu.cn

    地址:广东省广州市新港西路135号 邮政编码:510275 【管理登陆