报 告 人：朱惠彪教授

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

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

报告所在：校本部东区盘算机大楼1001室

约请人：缪淮扣教授

报告摘要：

Verilog是一种硬件形貌语言，，，
，，在工业界获得普遍的应用。。。。多线程离散事务模拟语言MDESL是一种类似Verilog的语言，，，
，，具备许多特征，，，
，，如事务驱动盘算和共享变量并发等。。。。本次报告从理论与实践两方面出发，，，
，，研究怎样将MDESL的代数语义与操作语义相毗连并验证两者的等价性。。。。代数语义与操作语义凭证首规范式和派生战略相毗连，，，
，，派生的操作语义以定理的形式给出，，，
，，并凭证派生战略研究了操作语义的准确性与完整性。。。。别的，，，
，，在实践方面，，，
，，我们使用定理证实器Coq对代数语义和操作语义举行机械化编码，，，
，，并机械验证了派生的操作语义的准确性和完整性。。。。

报告人简介:

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