Home

Auto2证明自动化和程序验证中的应用


Speaker

詹博华, 中科院软件所

Time

2021-02-07 13:30:00 ~ 2021-02-07 15:00:00

Location

腾讯线上会议(会议ID:775 320 466;免密码)

Host

Qinxiang Cao

Abstract

      Auto2是一个在Isabelle中实现的证明自动化工具,其主要思想是基于最佳优先(best-first)的搜索方式和congruence closure数据结构的使用,因此结合了SMT和Resolution算法中的关键部分。Auto2的主要应用包括基于集合论的形式化数学,以及基于分离逻辑的程序验证。使用auto2,我们验证了多个算法和数据结构,以及其中一些算法和数据结构的时间复杂度分析。

在这次报告中,我将介绍Auto2的基本设计方案,以及如何应用于基于分离逻辑的程序验证。

Bio

      詹博华的研究方向是形式化方法,包括交互式定理证明和嵌入式系统的建模和验证。2014年博士毕业于普林斯顿大学数学系,之后在麻省理工学院和慕尼黑工业大学任博士后。2018年加入中科院软件所,现任副研究员。研究工作发表于CAV, IJCAR/CADE, TACAS, ITP, ICFEM, J. Automated Reasoning 等形式化方法领域的主要会议和期刊。

© John Hopcroft Center for Computer Science, Shanghai Jiao Tong University
分享到

地址:上海市东川路800号老虎机电玩城微信上下分软件大楼专家楼
邮箱:nmbfzs.com 电话:021-54740299
邮编:200240