能否通过逻辑编程消灭程序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
相关话题
config、option、setting这三者在程序世界里是什么区别？怎么写出一本程序员风格的修真小说？
程序员讲到底就是”增删改查“吗？
C# 如何在调用控件时做到 Thread-safe（线程安全）？
如何才能修炼成一名不可替代的程序员，避免裁员危机？
GitHub 上有哪些适合新手跟进的优质项目？
为什么 Linux 如此安全，却不把 Linux 设计成像 Windows 一样的图形界面来使用？
《三体》中对艾AA提出的请求“好歹再带两个男人”，睿智的罗辑为什么拒绝了？
如何评价领导要用代码行数衡量每个人的工作量？
关于《黄晓明PK屠呦呦：一生努力不敌一场作秀！》这篇文章应如何评价？
前一个讨论
自动驾驶车如何降低被黑客控制的风险？
下一个讨论
如何评价 Google Earth VR？
相关的话题
有哪些道理是你当了程序员后才知道的？国外的程序员是如何保养「革命的本钱」？
有多少人知道汉诺塔其实应该叫河内塔？
在职程序员们，如何看待高校学生的技术不断更新迭代？
真的有人是因为喜欢科研才读研的么？如果是，乐趣在哪？
有什么理论复杂但是实现简单的算法？
面试想拿 10K，HR 说你只值 7K，该怎样回答或者反驳？
你们周围有在 GitHub 、博客上很活跃，但工作收入并不是很好的码农吗？
法国亿万富翁筹资一亿美元在硅谷建立「免学费」大学启动「42」计划的目的是什么？
既然报个培训班就可以成为码农，那学计算机专业有什么用？
如何看待奥巴马呼吁每个美国人都学习编程？
如何看待「大部分程序员只会写三年代码」的说法？
比尔·盖茨的编程水平怎么样？算得上是大师级别吗？
为什么很多计算机上的阿拉伯数字零（0）中间都有一个斜杠（/）？
ROE比债务利率高是个什么逻辑？
国内教职还是美国码农？
程序中的堆和栈大小是动态变化的，还是相对固定的？
我怎样成为@vczh一样的大神？
蒋凡「疑似出轨张大奕」被除名合伙人，阿里程序员「通过内部代码抢月饼」被开除，如何看待二者的惩罚力度？
为什么程序都要用英文写，中文不行吗？
a=b则b=a，这是真理吗？有没有例外？
在计算机科学领域，为何不使用拼音代替英文做为关键字?
为什么GCC的版本号增速比以前快这么多？
你最痛苦的一次找程序 bug 的经历是哪次？
C++ 中，如果指针换了被指向的东西，那被指向的原来的东西（是被 new 出来的）所占的内存会立刻被释放吗？
逻辑性教育与思维在中国是不是较为缺少？
计算 2 的 64 次方有什么特殊技巧？
程序员如何有效、愉快的使用 GitHub？
黑客可以厉害到什么程度？
如何通过自学找到一份开发的工作？