ITR: Integrating Induction Schemes into Decision Procedures

ITR：将归纳方案纳入决策程序

基本信息

批准号：
0113611
负责人：
Deepak Kapur
金额：
$ 40.15万
依托单位：
University of New Mexico
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2001
资助国家：
美国
起止时间：
2001-07-15 至 2005-06-30
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=0113611&HistoricalAwards=false
关键词：
ITR Integrating Induction Schemes into

项目摘要

Verification tools based on decision procedures including OBDD based tools and model-checkers have been effectively used in many application areas including hardware verification, protocol analysis and verification, static analysis and type-checking of code, byte-code verification, analysis of mobile code and proof-carrying code. These tools are however unable to deal with computations modeled using large state space (including infinite state space), partly because they do not support inductive reasoning. Induction based theorem provers, while quite powerful, lack automation and require tremendous user guidance. A novel and radical approach is proposed to combine decision procedures, rewriting and induction schemes in a restricted way so as not to lose automation. Using this approach, recursive definitions are given as terminating rewrite rules on top of decidable theories, such as Presburger arithmetic. Induction schemes are generated from these terminating definitions. By imposing structure on recursive definitions, it becomes possible to automatically decide a large class of conjectures requiring inductive reasoning. It is proposed to extend and generalize this approach to consider a large class of recursively defined functions, their interactions with each other, as well as a large class of conjectures about these functions, that can be automatically decided (without any need for user guidance).

基于决策程序（包括基于OBDD的工具和模型检查器）的验证工具已在许多应用领域有效使用，包括硬件验证，协议分析和验证，静态分析和代码的类型检查，字节代码验证，移动代码和移动代码分析和分析证明代码。但是，这些工具无法处理使用大型状态空间（包括无限状态空间）建模的计算，部分原因是它们不支持归纳推理。基于归纳的定理掠夺虽然非常强大，但缺乏自动化，需要大量的用户指导。提出了一种新颖的激进方法，以限制方式将决策程序，重写和归纳方案结合在一起，以免失去自动化。使用这种方法，将递归定义作为终止在可决定理论之上的重写规则，例如前爆发算术。从这些终止定义产生了归纳方案。通过对递归定义施加结构，可以自动决定需要归纳推理的大量猜想。有人建议扩展和推广这种方法，以考虑一大批递归定义的功能，它们彼此的相互作用以及有关这些功能的大量猜想，可以自动确定（无需任何用户指导）。