Eager: Optimal Length Integer Resolution Refutation in UTVPI Constraints

Eager：UTVPI 约束中的最佳长度整数解析反驳

• 批准号: 1305054
• 负责人: Krishnamurthy Subramani
• 金额: $ 6.57万
• 依托单位: West Virginia University Research Corporation
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-07-01 至 2016-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1305054&HistoricalAwards=false
• 关键词: Eager; Optimal; Length; Integer; Resolution

Constraint solving is an integral part of program verification, in general and abstract interpretation in particular. This proposal exploressome fundamental issues in integer feasibility checking and certification for a specialized class of constraints called Unit Two Variable Per Inequality (UTVPI) constraints. This approach is based on fundamentally new insights into the problem of integer feasibility checking, and will provide actual certificates of infeasibility. The ability to provide positive and negative certificates will impact program verification, and enhance the reliability of software.This project uses a proof system called FMR (Fourier-Motzkin with Rounding), which is a sound and complete system for establishing the lattice point infeasibility of a UTVPI system. This work will isolate the smallest-sized proof of infeasibility in the FMR proof system with an appropriately defined notion of size, and will explore the problem of certification by trying to identify the form of certificates and optimize the size of such certificates.

约束求解是程序验证的一个重要组成部分，一般来说，特别是抽象解释。该建议探讨了整数可行性检查和认证的一个专门的一类约束称为单位二变量不等式（UTVPI）约束的一些基本问题。这种方法基于对整数可行性检查问题的全新见解，并将提供不可行性的实际证明。提供正证书和负证书的能力将影响程序验证，并提高软件的可靠性。本项目使用了一个称为FMR（Fourier-Motzkin with Rounding）的证明系统，这是一个完善的系统，用于建立UTVPI系统的格点不可行性。这项工作将隔离FMR证明系统中不可行性的最小尺寸的证明，并适当定义尺寸的概念，并将通过尝试识别证书的形式和优化此类证书的尺寸来探索认证问题。