邮箱登录 | 所务办公 | 收藏本站 | English | 中国科学院
 
首页 计算所概况 新闻动态 科研成果 研究队伍 国际交流 技术转移 研究生教育 学术出版物 党群园地 科学传播 信息公开
国际交流
交流动态
学术活动
学术交流
现在位置:首页 > 国际交流 > 学术活动
Using Coq for the formal verification of an Instruction Set Simulator
2017-05-27 | 【 【打印】【关闭】

  报告题目:Using Coq for the formal verification of an Instruction Set Simulator

  报告时间:2017年5月17日(周三)上午 10:30-12:00

  报告地点:计算所 1048室

  主讲人: Prof. Jean-Francois Monin,Professor,Polytech'Grenoble,University of Grenoble Alpes

  报告摘要:Coq is a very successful French proof assistant which won several international awards and is routinely taught in prestigious universities such as MIT, UPenn, Yale or Princeton. This talk will recall the basic features of Coq and present an application performed in the framework of a Sino-French cooperation : the formal verification of an Instruction Set Simulator for the ARM processor. This simulator, called SimSoC (Simulator of Systems on Chips) was designed and very efficiently implemented in C++ by another Sino-French team in LIAMA -- for instance, it is able to boot the linux OS. In order to secure the ISS --- one of the most sensitive parts of SimSoC, we formalized in Coq the behavior of the processor; next, we got the formal behavior of (a C version of) the ISS simulator from the operational semantics of C, formalized in Coq in the Compcert Inria project, and were able to prove that the simulator behaved accordingly to the Coq formal model. This is joint work with Xiaomu Shi, Frederic Blanqui, Claude Helmstetter and Vania Joloboff .

  主讲人简介:

  Jean-Fran?ois Monin has been a Professor of Computer Science at Polytech'Grenoble, University Grenoble Alpes since 2003, where he is currently the head of the Informatics Department. He is also the European Director of the LIAMA Sino-French laboratory. From 2009 to 2013 he has been awarded a CNRS research grant in LIAMA and Tsinghua University. Before 2003 he was at France Telecom R&D, where he led a research group devoted to formal methods and applied them successfully to prove the correctness properties of software devices in an industrial framework. His research work is devoted to the Coq type-theoretic proof assistant with applications on distributed algorithms, security issues and embedded software. Beyond research papers at IEEE TSE, SCP, FMSD,ICLP, FM, MPC, TYPES, ITP, FORTE, CPP, he published a book entitled "Understanding Formal Methods" covering the various state-of-the-art approaches in this hot area.

 

  

  

 
网站地图 | 联系我们 | 意见反馈 | 所长信箱
 
京ICP备05002829号 京公网安备1101080060号