λ演算与微处理器形式验证

摘要：

现代集成电路设计不但是一项软件工程,而且是一项证明工程.不断增长的集成电路复杂性迫使各芯片公司引入形式化方法进行芯片正确性证明.在这些证明工程中,以λ演算为基础的证明系统起着不可忽视的作用.本文将综述这些证明系统在微处理器形式验证中的应用情况.

关键词： λ演算 类型理论 形式验证 硬件设计 微处理器 集成电路

作者: 陈钢

作者单位: 美国波士顿

会议类型: 国内会议

会议名称: 2003”全国软件与应用学术会议

会议地点: 北京

会议语种:中文

页码: 94-99

在线出版日期: 2003-11-01（万方平台首次上网日期，不代表论文的发表时间）