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的工具和模型检查器已经有效地用于许多应用领域，包括硬件验证、协议分析和验证、代码的静态分析和类型检查、字节码验证、移动的代码和携带证明的代码的分析。 然而，这些工具无法处理使用大状态空间（包括无限状态空间）建模的计算，部分原因是它们不支持归纳推理。基于归纳的定理证明器虽然非常强大，但缺乏自动化，需要大量的用户指导。提出了一种新颖的和激进的方法，联合收割机结合决策过程，重写和归纳计划在一个限制的方式，以便不失去自动化。 使用这种方法，递归定义给出了终止重写规则的可判定的理论，如Presburger算法。归纳方案是从这些终止定义中产生的。通过在递归定义上强加结构，可以自动决定需要归纳推理的一大类结构。建议扩展和推广这种方法，考虑一个大类的递归定义的功能，它们之间的相互作用，以及一个大类的这些功能，可以自动决定（无需任何用户的指导）的apturtures。