能否通过逻辑编程消灭程序BUG？ 第1页
1
david-dong-20 网友的相关建议:
有很多人做啊，这就是形式化方法嘛。
以前听过微软研究院的人讲他们怎么把他们的工作，一个叫FORMULA 2.0的东西在微软内部做形式化验证，找到了USB3.0等等很多软件里的很多bug，效果蛮好的。
FORMULA - Modeling Foundations - Microsoft Research亚马逊也有用，使用TLA+去设计验证一些关键系统。
http:// research.microsoft.com/ en-us/um/people/lamport/tla/formal-methods-amazon.pdf然后就更不要提很多航天系统啊，对安全性要求高的系统用形式化方法的就更多了。
前些年发在SOSP上的被形式化验证过的操作系统内核SeL4。
http://www. sigops.org/sosp/sosp09/ papers/klein-sosp09.pdf这些还是已经到比较实用阶段的东西了，学术界还有更多更多的研究。
1
相关话题
为什么C没有布尔类型？如果编程语言有性别？Java、C++、C、C#是男是女?是GAY还是LES？
Visual Studio 是不是坑了一代人？为什么？
哪些Linux发行版适合普通用户使用？
从硅谷回国后有什么感想？
为什么很多人会觉得IT门槛低？
未来编程会不会成为一个人人都有的能力，从而程序员的高薪不再？
在计算机科学领域，为何不使用拼音代替英文做为关键字?
如何正确通过 C++ Primer 学习 C++？
如何使用 python 写一个简单的表达式解释器？
前一个讨论
自动驾驶车如何降低被黑客控制的风险？
下一个讨论
如何评价 Google Earth VR？
相关的话题
如何看待人口老龄化？请问有什么好的C语言面向对象的扩展的方式？最好是有比较好的项目的源码参考。
30硕士毕业，工作一年的码农，看不到前景，未来怎么办？要不要转行？
程序员中的单个方法的行数极限是几行？80？200？500？
计算机专业，名校毕业和普通学校毕业有什么区别？
理工科人士如果在相关知识和背景了解不多的情况下以肯定性的语气跨界讨论社科类问题，是否与科学精神相悖？
如何评价某985老师所说的「C语言至少学10年才能懂」?
程序员如何有效、愉快的使用 GitHub？
C#相对路径 连接Access数据库怎么写??
程序中的堆和栈大小是动态变化的，还是相对固定的？
如果代码按行付费，会有什么好玩的事情发生？
996.icu 关注者多又能怎样呢？会有实际的变化发生么？
逻辑悖论能不能证明一个命题的错误？
有哪些好笑的关于程序员的笑话？
该三段论的逻辑正确吗？
如果程序员每天都浅尝辄止地学一些不同的新技术，长久以往，人会变成什么样子呢？
老大只让用vi写代码该怎么破?
顶级的程序员是怎么样的？
一个27岁没文凭，想去努力自学编程，有机会成为程序员吗？
在公司里开发软件 和学校有什么不同？
链表和数组的插入删除时间复杂度都是o(n)，为什么教材网络上说链表效率高？
能否通过逻辑编程消灭程序BUG？
如何理解「由于脚本在服务器上执行，因此浏览器在不支持脚本的情况下就可以显示服务器端的文件」？
精通 Java 是一种怎样的体验？
23岁曾放弃编码，现想重新编码，我该如何做？
一名大二的计算机专业的学生，目前学了很多编程语言，但都学得很浅。是不是应该专攻一门感兴趣的语言？
如何反驳「我评论个冰箱还得会制冷吗」？
有哪些可以提高程序员技术档次的书或博客？
为什么程序比较难写、bug 比较难调呢？
技术发展是否也是一种原罪？