Model checking is a technique for verifying finite state concurrent systems such as sequential circuit designs and communication protocols. It has a number of advantages over traditional approaches that are based on simulation, testing, and deductive reasoning. In particular, model checking is automatic and usually quite fast. Also, if the design contains an error, model checking will produce a counterexample that can be used to pinpoint the source of the error. The method, which was awarded the 1998 ACM Paris Kanellakis Award for Theory and Practice, has been used successfully in practice to verify real industrial designs, and companies are beginning to market commercial model checkers. The main challenge in model checking is dealing with the state space explosion problem. This problem occurs in systems with many components that can interact with each other or systems with data structures that can assume many different values. In such cases the number of global states can be enormous. Researchers have made considerable progress on this problem over the last ten years. This is the first comprehensive presentation of the theory and practice of model checking. The book, which includes basic as well as state-of-the-art techniques, algorithms, and tools, can be used both as an introduction to the subject and as a reference for researchers. About the Authors Edmund M. Clarke, a pioneer of the automated method called Model Checking, is FORE Systems Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University, and a winner of the 2007 Turing Award given by the Association for Computing Machinery. Doron Peled is Professor of Computer Science at the University of Warwick, Coventry, UK. Endorsements "Model Checking is bound to be the pre-eminent source for research, teaching, and industrial practice on this important subject. The authors include the foremost experts. This is the first truly comprehensive treatment of a line of research that has gone from conception to industrial practice in only two decades." —R. P. Kurshan, Distinguished Member Technical Staff, Bell Laboratories
- 粉丝: 48
- 资源: 13
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- 27页智慧街道信息化建设综合解决方案.pptx
- 计算机二级Ms-Office选择题汇总.doc
- 单链表的插入和删除实验报告 (2).docx
- 单链表的插入和删除实验报告.pdf
- 物联网智能终端项目设备管理方案.pdf
- 如何打造品牌的模式.doc
- 样式控制与页面布局.pdf
- 武汉理工Java实验报告(二).docx
- 2021线上新品消费趋势报告.pdf
- 第3章 Matlab中的矩阵及其运算.docx
- 基于Web的人力资源管理系统的必要性和可行性.doc
- 基于一阶倒立摆的matlab仿真实验.doc
- 速运公司物流管理模式研究教材
- 大数据与管理.pptx
- 单片机课程设计之步进电机.doc
- 大数据与数据挖掘.pptx
评论30