时间: 3月29日（周二）15:10-18:00
地点: 三教101
主讲人：贺飞（清华大学软件学院）
贺老师将向大家介绍他最近在形式化验证方面的工作。
主要内容如下：
1. BDD-Based Assume-Guarantee Reasoning through Implicit Learning
Abstract. We present a purely BDD-based assume-guarantee reasoning technique to improve the scalability of symbolic model checking. The new technique adopts a BDD learning algorithm to generate BDD’s as contextual assumptions. A new witness analysis algorithm is proposed to exploit the multitude of traces returned by symbolic model checkers.
Using the classi?cation tree-based BDD learning algorithm to generate contextual assumptions, we compare assume-guarantee reasoning with monolithic symbolic model checking. The new technique always infers smaller contextual assumptions than contexts in our experiments.
2. On Array Theory of Bounded Elements
Abstract. We investigate a ?rst-order array theory of bounded elements. By reducing to weak second-order logic with one successor (WS1S), we show that the proposed array theory is decidable. Finally, two natural extensions to the new theory are shown to be undecidable.
贺飞老师是清华大学计算机系2008届博士，自2008年起至今在清华大学软件学院任教。
这是他的个人主页：http://www.thss.tsinghua.edu.cn/docinfo/board/boarddetail.jsp?columnId=00105040301&parentColumnId=001050403&itemSeq=5214