科学网—ymin的博文 - 第17页

设为首页收藏本站

开启辅助访问切换到宽版

科学网 › 我的中心 › 博文 › ymin的博文

ymin

https://wap.sciencenet.cn/?290937

学术导航| 做学问| 微电子| 计算机| 科研管理| 杂谈| 网络|

第一届多处理器系统芯片设计验证测试北京都市研讨会（100109）: 闵应骅 2010-1-9 15:08; 第一届多处理器系统芯片设计验证测试北京都市研讨会（100109）闵应骅 1月6日，冒着严冬的寒风和大雪，40多人来到北京师范大学英东楼参加第一届多处理器系统芯片设计验证测试北京都市研讨会（MPSoC研讨会）。这个会是由北师大骆祖莹副教授发起，得到计算所李晓维研 ...; 个人分类: 微电子|3747 次阅读|没有评论

未来互联网体系结构（100103）: 闵应骅 2010-1-3 11:32; 未来互联网体系结构（100103）闵应骅未来互联网体系结构的问题为大家所关心，政府关心、中国科学院关心、基金委关心、社会各方面都关心。许多专家为此出主意。这牵涉到以后的大批科研经费、大量的科研课题。老早就有题目叫下一代互联网。有人提出来现在应该搞互联网下一代&rdqu ...; 个人分类: 杂谈|4376 次阅读|2 个评论

模型检验（结束语）（100101）: 闵应骅 2010-1-1 15:24; 模型检验（结束语）（100101）闵应骅学习完模型检验(model checking)三位创建者的文章以后，现在可以说几句结束语了。科学大家就是科学大家。他们就模型检验28年来的发展，对历史、研究动机、已有成就及今后发展做了高度的概括和总结，指明了方向。但是，真要想做这方面的研究， ...; 个人分类: 学术导航|4305 次阅读|没有评论

模型检验（5）（100101）: 热度 2 闵应骅 2010-1-1 14:23; 模型检验（5）（100101）闵应骅模型检验(model checking)自从1981年提出来以后，受到各种非议。至今28年过去了，才得到了学术界和工业界的广泛关注。这是很正常的。要求一个学术成果马上用于实际，很不现实。中国某些干部就这么急功近利。算法的设计验证包括三步：（1）需求规范；（2）建立可执行的 ...; 个人分类: 学术导航|3756 次阅读|1 个评论热度 2

模型检验（4）（091231）: 闵应骅 2009-12-31 17:25; 模型检验（4）（091231）闵应骅模型检验的成功之处在于它用自动搜索代替手动证明来解决验证的问题。模型检验包括三部分：1。基于命题时态逻辑的规范语言，2。表示被验证系统的编码状态机的方法，3。验证算法，对状态空间的智能搜索以确定规范是真还是假。如果规范没有被实现，模型检验能够给出反例。 ...; 个人分类: 学术导航|6503 次阅读|没有评论

模型检验（3）（091231）: 闵应骅 2009-12-31 11:36; 模型检验（3）（091231）闵应骅时态逻辑用来描述正确的系统行为，模型检验提供实用的硬件和软件验证方法。模型验证可形式地描述如下：给定一个有限结构M，状态s，和一个时态逻辑公式，问M, s |= f ?即问：在结构M中，于状态s0，f是否为真？或者说，给定M和f,计算这个集合{s : M, s |= f}。他们证明了 ...; 个人分类: 学术导航|4830 次阅读|没有评论

模型检验（2）（091231）: 闵应骅 2009-12-30 17:17; 模型检验（2）（091231）闵应骅程序正确性的形式验证依靠数学逻辑的使用。程序是一个很好定义了的、可能很复杂、直观上不好理解的行为。而数学逻辑能精确地描述这些行为。过去，人们倾向于正确性的形式证明。而模型检验回避了这种证明。在上世纪60年代，流行的是佛洛伊德-霍尔式的演绎验证。这种办法 ...; 个人分类: 学术导航|5390 次阅读|没有评论

模型检验（1）（091230）: 闵应骅 2009-12-30 10:23; 模型检验（1）(091230）闵应骅大家承认，计算机领域的ACM图灵奖相当于自然科学的诺贝尔奖。2007年图灵奖授予Edmund M. Clarke，E. Allen Emerson,和Joseph Sifakis。他们创立了模型检验---一种验证技术，用算法的方式确定一个硬件或软件设计是否满足用时态逻辑表述的形式规范。如果不能满足，则提供 ...; 个人分类: 学术导航|5544 次阅读|没有评论

关于域名服务器（091216）: 闵应骅 2009-12-16 09:03; 关于域名服务器（091216）闵应骅域名服务器（DNS）的效率和安全是大家都关心的问题。DNS是一个分等级的、分布式的、自治的、可靠的数据库。它服务于全世界。每一个TCP/IP包括Web页的信息流都从至少一个域名服务器的交易开始。一个内容分布网络（CDN）直接指向某个Web浏览器，需 ...; 个人分类: 计算机|3860 次阅读|没有评论

计算机编程的公理化基础（091206）: 闵应骅 2009-12-6 10:36; 计算机编程的公理化基础（091206）闵应骅大家知道，在1960年代，最著名的计算机程序语言是ALGOL60，基于精美而严格的语法，形式化为一种上下文无关语言。然而，语义更重要，但并没有形式化。英国人相信，形式化应该包含一组公理，使程序员能写出正确而有效的程序。但这个想法本身就无法反映不断前进 ...; 个人分类: 计算机|4482 次阅读|没有评论

1 ... 11 12 13 14 15 161718 19 下一页

会议

Archiver|手机版|科学网 ( 京ICP备07017567号-12 )

GMT+8, 2024-5-17 15:37

Powered by ScienceNet.cn

Copyright © 2007- 中国科学报社

返回顶部