能否通过逻辑编程消灭程序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
相关话题
为什么国家定义程序员为新生代农民工，而不是高端或科技人才，这说明程序员门槛低吗？集中全世界程序员的力量，可以在三天之内实现一个手机淘宝吗？
面试想拿 10K，HR 说你只值 7K，该怎样回答或者反驳？
在出现事故之前悄悄排除了一个重大BUG，是怎样的一种体验？
为什么老板要教我们做互联网的程序员不要把工作和生活分开，这对于独立的程序员个体有什么好处？
学习编程会让人的性格发生变化吗？
为什么不少人习惯谴责强奸案中的受害者？
晚上脑子里也想着bug，睡不好怎么办？
什么样的程序员才是牛逼的程序员？
java为什么不支持泛型数组？
前一个讨论
自动驾驶车如何降低被黑客控制的风险？
下一个讨论
如何评价 Google Earth VR？
相关的话题
你的编程能力从什么时候开始突飞猛进？“民主之后杀你全家”有没有合理性？
「传输自动生成代码并执行、生成所需文件」能否成为未来的下载方式？
Oracle、SAP、Github 暂停俄罗斯业务，Github 否认，此次限制会有多大影响？
有没有可能现在设计一个程序语言，它能够充分吸收现存语言的优点，同时排除那些缺点？
什么是 Agile Software Development（敏捷软件开发）？
程序员有流派吗？
如果有一个东西存在，但我们永远无法发现 ，那么这个东西本身并没有任何意义吗？
程序员怎么赚钱?
中国不教逻辑学吗？为什么？
计算机系学生应该怎样正确管理自己的电脑？
诸葛亮的逻辑有几层？
什么是寄存器压栈？栈是内存的一部分，寄存器是cpu一部分，怎么压？
国内程序员如何获得北美的程序员工作机会？
程序员为什么越老越贬值的厉害？
有哪些有趣的反爬虫手段？
说程序员毫无难度的人，到底是不是在装13？
公司拖欠后端工资逼急了可以删库跑路，逼急了前端该如何何去何从？
各个学科或领域中，有哪些“自我指涉”现象？
打字速度对编程的影响大吗？
会有公司要一个接近40岁，水平不高，但只要应届生一半工资的程序员吗？
除了跨平台和平台成本以外，Java 还有什么特性是 C# 不具备的？
如何在运行时初始化静态成员变量？
数学差的关键原因是缺乏抽象思维还是逻辑性弱？
有哪些只有程序员才能 get 到笑点的故事？
可以用最通俗的语言告诉我程序员敲的一行行代码怎么变成一个个游戏？那么写代码的难度又在哪里？
如何追到湾区码农小哥哥?
为什么 Windows 系统 Program Files 这个经常用来装软件的目录，名称中有个空格？
一个浮点数到底是怎么被转换为字符串输出？一个浮点数不精确，那么其输出的值是怎么被确定的呢？
为什么女性程序员少于男性，因为女性不适合写程序吗？