Using Coq for the formal verification of an Instruction Set Simulator
发布时间:2017-06-09 15:09:19

报告题目: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.