报 告 人：朱惠彪教授

单位：华东师范大学计算机科学与软件工程学院

报告时间：2019年5月30日（周四）14：30～16:00

报告地点：宝山校区计算机大楼1001室

邀请人：缪淮扣教授

报告摘要：

Verilog是一种硬件描述语言，在工业界得到广泛的应用。多线程离散事件模拟语言MDESL是一种类似Verilog的语言，具备很多特性，如事件驱动计算和共享变量并发等。本次报告从理论与实践两方面出发，研究如何将MDESL的代数语义与操作语义相连接并验证两者的等价性。代数语义与操作语义根据首规范式和派生策略相连接，派生的操作语义以定理的形式给出，并根据派生策略研究了操作语义的正确性与完备性。此外，在实践方面，我们使用定理证明器Coq对代数语义和操作语义进行机械化编码，并机械验证了派生的操作语义的正确性和完备性。

报告人简介:

朱惠彪,华东师范大学计算机科学与软件工程学院教授，博士生导师，教育部软件工程专业教学指导委员会委员，中国计算机学会形式化方法专业委员会副主任。研究方向为高可信计算、形式化方法和信息物理融合系统。在国际著名期刊和会议发表论文170余篇，曾主持自然科学基金委中丹国际合作项目“信息物理融合系统的基础研究”（2011-2013）并且获得滚动资助（2014-2016）。“基于模型的可信软件理论与开发方法”获得2011年度教育部高等学校自然科学一等奖（第二完成人）, 分别于2013年和2017年获得高等教育上海市教学成果奖特等奖和一等奖（排名第二和第五），于2018年9月获得国家教学成果奖二等奖（排名第五）。