能否通过逻辑编程消灭程序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
相关话题
阿里巴巴 P8、P9 及以上到底是什么水平？有哪些编程上的中文术语让人困惑，但是看英文就一目了然的？
2019 年了，C# 发展得怎么样了？
如何反驳与自己观点（或立场）相同但缺乏逻辑的人？
计算机中为何不直接使用 UTF-8 编码进行存储而要使用 Unicode 再转换成 UTF-8 ？
代码结构中Dao，Service，Controller，Util，Model是什么意思，为什么划分？
算法书如何选择？
作为一名 IT 技术牛人是一种怎样的体验？
只靠读代码 debug 不会单步调试能当编程高手吗？
请问如何判断自己适不适合当程序员？
前一个讨论
自动驾驶车如何降低被黑客控制的风险？
下一个讨论
如何评价 Google Earth VR？
相关的话题
如何向外行解释产品经理频繁更改需求为什么会令程序员烦恼?不同编程语言的程序员之间有鄙视链么？
如何评价这位法学生针对最近一系列负面新闻的言论？
编程新手如何提高编程能力？
编程那么难，为什么不弄一个大众一学就会的计算机语言呢?
有什么在线的编程游戏？
怎样看待王垠的《我和 Google 的故事》？
如何反驳「太平洋又没加盖，那么xx，有本事自己游过去」？
我在编程时给变量命名总觉得困难，有没有什么实用技巧?
程序员该选择Macbook Pro吗？
作为程序员，你有哪些正在做的个人项目？
为什么不流行国语编程？
为什么 Windows 系统 Program Files 这个经常用来装软件的目录，名称中有个空格？
如何理解 “c++缺少对象级别的消息发送机制” 这句话？
为什么很多人喜欢 Python？
Java里面的封装是不是多此一举？
C# 这么优秀的语言，现在到底出了什么问题？
中文编程目前面临的难题是什么，你有哪些建议？
如果要给编程语言加上一种可用于计量运算的基本数字类型，你觉得该怎么设计这种计量类型，以及修改语言本身？
程序员月薪一万到底有多难？
如何证明自己不在「楚门的世界」里？
C++ 实现接口与实现分离后，文件变得更多了，到底有什么好处？
怎样评价《数码宝贝》第一部中的泉光子郎的编程水平？
为什么国内创造不出很棒的编程语言？
C++ 实现接口与实现分离后，文件变得更多了，到底有什么好处？
既然有指针了，为什么c++还搞个引用出来？
程序员如何保持技术敏感度？
如何看待知乎前后端关注度差距悬殊的现象？
集中全世界程序员的力量，可以在三天之内实现一个手机淘宝吗？
如何寻找热爱编程而且有经验的程序员？