清华大学操作系统讲座

2016年5月24日，耶鲁大学计算机系教授邵中老师在清华大学FIT大楼进行了操作系统验证方面的讲座。讲座由北京迪捷数原科技有限公司的首席科学家陈渝老师主持，公司多名研发工程师均参加了此次讲座。

讲座中，邵老师介绍了对操作系统做形式化验证的思路。他认为，首先要对操作系统进行进行合理分层和模块化，然后对每个层次和每个模块建立deepspec，这样会让整个操作系统的形式化证明更加简单可行。 讲座结束后，迪捷数原的工程师就代码自动生成工具ModelCoder中用到的形式化技术和邵老师进行了交流和讨论，邵老师详细说明了形式化技术在学术界的最新发展。    

关于邵中老师

邵中老师，中国科大“大师讲席”教授。1983年进入中国科学技术大学少年班，1988年毕业于计算机系，获计算机科学学士学位；1994年毕业于普林斯顿大学，获计算机科学博士学位。1994年至今在耶鲁大学计算机系任教，2003年起任耶鲁大学教授。现任中科大－耶鲁高可信软件联合研究中心主任。