讲座题目:可信计算论坛：Formal Verification of Imperative Programs: the North Face

主讲人:Jean-Francois Monin教授

主持人:陈仪香教授

开始时间:2012-12-04 15:00

讲座地址:中北校区数学馆201报告厅

主办单位:软件学院和科技处

报告人简介：

    Short Bio,Jean-Franois Monin has been a professor of Computer Science atUniversity Joseph Fourier, Grenoble since 2003. Formerly hewas at France Telecom R&D, where he led a research group devoted toformal methods and applied them successfully to prove the correctness properties of software devices in an industrial framework.

Since 2009,he has been awarded a CNRS research grant in the LIAMA Sino-French laboratory, at Tsinghua University, where he works with the Coqtheoretic-type proof

assistant with applications on distributedalgorithms,security issues and embedded software

报告内容简介：

    The problem of verifying imperative programs has been raised from thevery beginning of Computer Science by Turing himself. A populartechnique initiated by Floyd and Hoare in the 1960's, is based onassertions about the state of a program expressed in a high-level language. Such technique are known to scale-up to complex programminglanguages such as C or Java. However, current implementations sufferfrom some limitations that we will discuss: their ability to cope withcomplex properties and the extent of the guarantee we obtain. Therefore, we consider an alternative approach, using operationalsemantics rather than axiomatic semantics. This approach is illustrated on our current experiments, performed at LIAMA/FORMES, based on the formal semantics of C as defined for the Compcert certified compiler.