• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>International Conference on Computer Aided Verification(CAV 2006); 20060817-20; Seattle,WA(US) >Termination Analysis with Calling Context Graphs
【24h】

Termination Analysis with Calling Context Graphs

机译：带有调用上下文图的终止分析

获取原文
获取原文并翻译 | 示例
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

We introduce calling context graphs and various static and theorem proving based analyses that together provide a powerful method for proving termination of programs written in feature-rich, first order, functional programming languages. In contrast to previous work, our method is highly automated and handles any source of looping behavior in such languages, including recursive definitions, mutual recursion, the use of recursive data structures, etc. We have implemented our method for the ACL2 programming language and evaluated the result using the ACL2 regression suite, which consists of numerous libraries with a total of over 10,000 function definitions. Our method was able to automatically detect termination of over 98% of these functions.
机译：我们介绍了调用上下文图以及各种基于静态和定理证明的分析，它们共同提供了一种强大的方法来证明用功能丰富的一阶函数式编程语言编写的程序的终止。与以前的工作相比，我们的方法是高度自动化的，并且可以使用此类语言处理循环行为的任何来源，包括递归定义，相互递归，使用递归数据结构等。我们已经为ACL2编程语言实现了我们的方法并进行了评估使用ACL2回归套件得到的结果，该套件由众多库组成，总共包含10,000多个函数定义。我们的方法能够自动检测这些功能中超过98％的终止。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号