百科问答小站 logo
百科问答小站 font logo



能否通过逻辑编程消灭程序BUG? 第1页

  

user avatar   david-dong-20 网友的相关建议: 
      

有很多人做啊,这就是形式化方法嘛。

以前听过微软研究院的人讲他们怎么把他们的工作,一个叫FORMULA 2.0的东西在微软内部做形式化验证,找到了USB3.0等等很多软件里的很多bug,效果蛮好的。

FORMULA - Modeling Foundations - Microsoft Research

亚马逊也有用,使用TLA+去设计验证一些关键系统。

research.microsoft.com/

然后就更不要提很多航天系统啊,对安全性要求高的系统用形式化方法的就更多了。

前些年发在SOSP上的被形式化验证过的操作系统内核SeL4。

sigops.org/sosp/sosp09/

这些还是已经到比较实用阶段的东西了,学术界还有更多更多的研究。




  

相关话题

  请各位前辈指导下简练代码的思路? 
  请问各位程序员,是我的思维方式有错误吗? 
  如何自学 Android 开发? 
  女程序员想自学SQL,前途和难度如何? 
  跪求!作为医生如何反驳程序员工资高? 
  为什么物理科普读物读起来津津有味,计算机科普却很枯燥且很少见? 
  程序员最理想的工作环境应该是什么样的? 
  Lisp 程序员的出路在哪里? 
  为什么说用了10年C++的程序员也不敢说自己精通C++? 
  作为计算机专业学生,最应该学习的课程前五位是什么? 

前一个讨论
自动驾驶车如何降低被黑客控制的风险?
下一个讨论
如何评价 Google Earth VR?





© 2025-04-04 - tinynew.org. All Rights Reserved.
© 2025-04-04 - tinynew.org. 保留所有权利