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

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

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