形式验证简介 - 计算机科学国家重点实验室.ppt

《形式验证简介 - 计算机科学国家重点实验室.ppt》由会员分享，可在线阅读，更多相关《形式验证简介 - 计算机科学国家重点实验室.ppt（10页珍藏版）》请在得力文库 - 分享文档赚钱的网站上搜索。

1、1,模型检测Model Checking,中国科学院软件研究所计算机科学国家重点实验室张文辉http:/ Schnoebelen. The Complexity of Temporal Logic Model Checking. Advances in Modal Logic 2002: 393-436.R. Jhala and R. Majumdar. Software Model Checking. ACM Computing Surveys 41(4), Article 21, 2009.-E. M. Clarke, O. Grumberg and D. A. Peled. Model

2、Checking. MIT Press, 1999.,6,参考文献,A. W. To and L. Libkin. Recurrent Reachability Analysis in Regular Model Checking. LPAR 2008: 198-213.S. La Torre, P. Madhusudan and G. Parlato. Model-Checking Parameterized Concurrent Programs Using Linear Interfaces. CAV 2010: 629-644.A. Cimatti, A. Micheli, I. Na

3、rasamdya and M. Roveri. Verifying SystemC: a Software Model Checking Approach. FMCAD 2010: 51-59.T. Launiainen, K. Heljanko, T. A. Junttila. Efficient model checking of PSL safety properties. IET Computers & Digital Techniques 5(6): 479-492. 2011.Naoki Kobayashi, Ryosuke Sato, Hiroshi Unno: Predicat

4、e abstraction and CEGAR for higher-order model checking. PLDI 2011: 222-233.,7,Ph. Schnoebelen: The Complexity of Temporal Logic Model Checking. Advances in Modal Logic 2002: 393-436,8,R. Jhala, R. Majumdar.Software Model Checking.ACM Computing Surveys 41(4), Article 21, 2009.,9,E. M. Clarke, O. Grumberg and D. A. Peled. Model Checking. MIT Press, 1999.,课程目标,掌握模型检测基础理论不同类型的模型不同类型的时序逻辑各种模型检测问题复杂性及模型检测算法具备模型检测方法研究及应用的能力能够较快阅读本专业方向的文献能够针对特定问题设计模型检测算法能够应用模型检测方法和工具对特定问题进行验证,