能否通过逻辑编程消灭程序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++缺少对象级别的消息发送机制” 这句话？
“受害人没有提出维权或反抗，你有什么资格（理由）代替他/她维权”这种观点逻辑有问题吗？如何反驳？
优化代码中大量的if/else，你有什么方案?
是否有多人认为程序员的工作就是复制粘贴？为什么？
如果存在世界的观测者，那么他要怎么向他人证明自己的身份？
当程序员鼓励师是什么样的体验？
为什么那么多公司不用 .NET，而选择 PHP、JSP，是 .NET 有什么缺点吗？
如何评价现在GitHub上一些非软件开发性质项目增多的风气？
后端开发除了增删改查还有什么？
前一个讨论
自动驾驶车如何降低被黑客控制的风险？
下一个讨论
如何评价 Google Earth VR？
相关的话题
《三体》系列小说中有哪些物理或逻辑 Bug？中国的程序员群体是否已经过多了？
为什么国内技术社区的影响力越来越弱呢？
如何看待百度于2017年2月28日晚疑似停止服务？
如何评价冯大辉（Fenng）的新文《聊聊 996》？
中医黑们说逻辑、实证、良心、判断力支持黑中医，但是我这中医粉，也是这些原因支持中医，为何会如此不同？
不适合编程的人是怎样的？
在公司里开发软件 和学校有什么不同？
如何评价《鸟哥的Linux私房菜》说BSD和GPL很类似以及Windows不跨处理器架构等内容？
程序员的穿搭真的是清一色格子衬衫吗？
程序员们有什么好的编程习惯？
为什么逻辑学的排中律不是任何条件下都可使用的?
喜欢用图形界面而不喜欢用命令行的人是不是不适合当程序员？
C# 这么优秀的语言，现在到底出了什么问题？
程序员为什么要一直写bug ，不能一次性写好吗？
代码之间为什么要加空格？
程序员35岁之后不写程序了，该怎样职业规划？
前端同事被富婆包养了，在深圳买了房，他代码技术远不如我，现在心里很不平衡，如何调节自己？
编程代码不会,无人可请教,甚至没有标准答案,该怎么办?
设计模式是不是有点太「玄」了？
有没有人能将知乎上的技术大牛都组织起来，做一个开源项目？比如实现一个CoreOS这样的东东
C#中字符串可以使用可变大小的内存，为什么数字不能？
如何评价螃蟹科技的这份《告游戏行业全体同仁书》？
为什么 Java 份额那么高，在知乎的存在感却不如 Python？
为什么有的高级程序员很讨厌甚至禁止使用 setTimeout？
怎么找到喜欢程序员的妹子做女友？
JetBrains 2022的远程功能和VSCode Remote相比如何？
为什么维基百科没有符合中国人的捐款方式？
要学 Python 需要怎样的基础？
为什么著名的轮子很少有用 Lisp 写的？