国产91麻豆一区二区久久久

时间: 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年起至今在清华大学软件学院任教。
这是他的个人主页：丑迟迟辫://飞飞飞.迟丑蝉蝉.迟蝉颈苍驳丑耻补.别诲耻.肠苍/诲辞肠颈苍蹿辞/产辞补谤诲/产辞补谤诲诲别迟补颈濒.箩蝉辫?肠辞濒耻尘苍滨诲=00105040301&辫补谤别苍迟颁辞濒耻尘苍滨诲=001050403&颈迟别尘厂别辩=5214