????

  
首页-科学研究_学术预告

学术报告440:MDESL的操作语义和代数语义连接的理论与实践

发布日期:  2019/05/27  周时强   浏览次数: 部门: 未知   返回

贝博体育报 告 人:朱惠彪教授

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

贝博体育报告时间:2019年5月30日(周四)14:30~16:00

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

邀请人:缪淮扣教授

报告摘要:

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

贝博体育报告人简介:

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

 

上一条:学术报告441:列车控制系统智能预测

下一条:学术报告439:智能系统软硬件优化设计