您当前的位置:首页 > 合作交流 > 学术活动 >
Jean-François Monin教授来实验室做报告
时间:2017-06-14 02:31:57      点击 :次      来源:      收藏

Jean-François Monin是法国Polytech’Grenoble University教授,系主任,他也是LIAMA中法实验室欧洲方的主任。

Jean-François Monin2017517日(星期三)上午1030-1230在计算所10层会议室做了题为“Using Coq for the formal verification of an Instruction Set Simulator”的学术报告。

Jean-François Monin教授在报告中回顾了Coq的基本特征,介绍了Coq的一个应用:形式化验证一个ARM处理器的指令级模拟器(Instruction Set SimulatorISS)。这个应用是中法合作的一部分。ISSSimSoC最敏感的部分。SimSoC 是中法合作的另外一个团队用C++开发的,可以引导Linux操作系统。为了验证ISSCoq首先形式化刻画了处理器指令的行为,接着获得ISS的形式化行为,然后证明模拟器的行为与Coq的形式化模型一致。Coq是一个非常成功的证明辅助工具,赢得了很多国际大奖,在一些知名大学如MITUPenn, Yale Princeton被作为课程内容讲授。

报告之后,参会的老师和同学就报告相关的问题进行了讨论。感谢Jean-François Monin教授带来的这次精彩报告。