能否通过逻辑编程消灭程序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
相关话题
程序员所积累的编程知识在十年后将有多少变得没用？为什么知乎用户 vczh 不建议初学编程的人把 C 作为入门语言？
你们周围有在 GitHub 、博客上很活跃，但工作收入并不是很好的码农吗？
代码初学者，学到一段时间后，怎么寻找练手的项目？
中文编程什么时候才能在中国崛起？英文编程是不是总有一个学习转换的过程使慢一拍？
985 本硕（上海交大）想走社招转行当程序员，为何频频被拒？
怎么找到喜欢程序员的妹子做女友？
为什么程序员会有代码能跑就不要动的观点？
学编程什么的需要专业版Windows吗？
如果软件正在占领全世界，为什么程序员得不到尊重？
前一个讨论
自动驾驶车如何降低被黑客控制的风险？
下一个讨论
如何评价 Google Earth VR？
相关的话题
有哪些事实没有一定计算机知识的人不会相信？程序员能纯靠技术渡过中年危机吗？
为什么说 zsh 是 shell 中的极品？
C#为什么非要把函数叫方法？
如何评价冯大辉（Fenng）的新文《聊聊 996》？
最难调试修复的 bug 是怎样的？
作为一个程序员，你的桌子上都有些什么？
程序员如何体会妹子换衣服的心情？
学 Python 都用来干嘛的？
数学/算法：正方形内有5个点，为什么最近点对的距离小于边长？
如果用进步次数评定一个人的成绩，如何获取第一名？
30 岁了，银行职员，想开始学习 JAVA 做回程序员，不知道来得及吗？
程序员35岁失业，为什么还那么多人建议学计算机？
如何评价「所有的失败都是当事者能力不足导致的」这句话？
如何看待国内地图行业更新政策商用api每年需支付5w元？
有哪些看似思维严密的背后有巨大的逻辑漏洞的事？
如何评价 C++ 11 auto 关键字？
为何网上充斥着程序员们各种“主义”之争？
在顶级游戏开发的过程中需要怎样的编程实力？
为什么别的职业都是越老越值钱，唯独程序员越老越容易失业？
有什么行为习惯昭示着你是个编程大佬？
如何看待 WebAssembly 这门技术？
代码全是调包的，怎么申请专利？
为什么这么多人吐槽996，还要去BAT等互联网公司体验福报？
哪段代码最能代表程序员的暴力美学？
突然想开一家程序员主题的餐馆，名字就叫程序员的菜，菜名就叫各种语言中的关键字，各位指点一哈，有前途没？
谁能用大妈听得懂的话解释一下什么是归纳与演绎？
字节跳动面试难吗，应该如何应对？
如何评价新浪一位程序员因加班未到现场，错失了年会 77 万特等奖？
程序员如何快速工资翻倍?