资料下载
程序验证研究综述
分享资料个
自20世纪60年代以来，虽然有Floyd-Hoare逻辑的出现，但使用形式化工具对命令式程序的正确性和可靠性进行自动验证。一直被认为是极具挑战性、神圣不可及的工作．20世纪末，由于更多科研的投入，特别是微软、IBM等大型公司研发部门的大量人力、物力的投入，程序验证方面在21世纪初取得了不少进展，例如用于验证空客代码无运行时错误的ASTREE工具、用于Windows设备驱动里关于过程调用的协议验证的SLAM工具．但这些工具并没有考虑动态创建的堆（heap）：ASTREE工具假设待验证代码没有动态创建的堆，也没有递归：SLAM假设待验证系统已经有了内存安全性．事实上，很多重要的程序，例如Linux内核、Apache、操作系统设备驱动程序等，都涉及到对动态创建堆的操作．如何对这类操作堆的程序（heap-manipulating programs）进行自动验证仍然是一个难题．2001年-2002年，分离逻辑（separation logic）提出后，其分离（separation）思想和相应的框（frame）规则使得局部推理Oocalreasoning）可以很好地应用到程序验证中．自2004年 以来，基于分离逻辑对操作动态创建堆的程序进行自动验证方面的研究有了很大的进展，取得了很多令人瞩目的成果，例如Spacelnvader/Abductor， Slayer， HIP/SLEEK，CSL等工作．着重对这方面的部分重要工作进行阐述．
声明：本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人，不代表电子发烧友网立场。文章及其配图仅供工程师学习之用，如有内容侵权或者其他违规问题，请联系本站处理。 举报投诉
- 相关下载
- 相关文章
