全国论文买卖去年销售额近10亿吗？（100105）

闵应骅 2010-1-5 11:51

全国论文买卖去年销售额近10亿吗？（100105） 闵应骅 新浪网上发了一条要闻：研究者称全国论文买卖去年销售额近10亿（http://www.sina.com.cn 2010年01月05日00:43 汉网-长江日报 ）。本人对此持怀疑态度。 要闻说：沈阳和他的团队开展了3年多的 ...

个人分类: 杂谈|4351 次阅读|1 个评论

未来互联网体系结构（100103）

闵应骅 2010-1-3 11:32

未来互联网体系结构（100103） 闵应骅 未来互联网体系结构的问题为大家所关心，政府关心、中国科学院关心、基金委关心、社会各方面都关心。许多专家为此出主意。这牵涉到以后的大批科研经费、大量的科研课题。老早就有题目叫下一代互联网。有人提出来现在应该搞互联网下一代&rdqu ...

个人分类: 杂谈|4336 次阅读|2 个评论

模型检验（结束语）（100101）

闵应骅 2010-1-1 15:24

模型检验（结束语）（100101） 闵应骅 学习完模型检验(model checking)三位创建者的文章以后，现在可以说几句结束语了。 科学大家就是科学大家。他们就模型检验28年来的发展，对历史、研究动机、已有成就及今后发展做了高度的概括和总结，指明了方向。但是，真要想做这方面的研究， ...

个人分类: 学术导航|4261 次阅读|没有评论

模型检验（5）（100101）

热度 2 闵应骅 2010-1-1 14:23

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

个人分类: 学术导航|3720 次阅读|1 个评论 热度 2

模型检验（4）（091231）

闵应骅 2009-12-31 17:25

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

个人分类: 学术导航|6453 次阅读|没有评论

模型检验（3）（091231）

闵应骅 2009-12-31 11:36

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

个人分类: 学术导航|4777 次阅读|没有评论

模型检验（2）（091231）

闵应骅 2009-12-30 17:17

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

个人分类: 学术导航|5351 次阅读|没有评论

模型检验（1）（091230）

闵应骅 2009-12-30 10:23

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

个人分类: 学术导航|5494 次阅读|没有评论

虚荣心（091227）

闵应骅 2009-12-27 16:14

虚荣心（091227） 闵应骅 最近看到《报刊文摘》上发表《环球时报》的一篇文章：中国演出镀金维也纳金色大厅遭质疑，很有感触。文章说：近年来，出租给外国演出团体让金色大厅成为了一个真正的金钱大厅，不仅演出经纪公司可以运作到金色大厅的演出， ...

个人分类: 杂谈|3101 次阅读|1 个评论

本页有 1 篇博文因作者的隐私设置或未通过审核而隐藏