Eager: Optimal Length Integer Resolution Refutation in UTVPI Constraints

约束求解是程序验证中不可或缺的一部分，特别是抽象解释。该方案探讨了一类特殊约束的整数可行性检验和证明中的一些基本问题，这类约束被称为单位二变量按不等式(UTVPI)约束。这种方法是基于对整数可行性检查问题的全新见解，并将提供实际的不可行性证明。提供正反证书的能力将影响程序验证，提高软件的可靠性。本项目使用了一个名为FMR(傅立叶-莫茨金舍入)的证明系统，它是一个完善的系统，用于建立UTVPI系统的格点不可行性。这项工作将利用适当定义的大小概念来分离FMR证明系统中不可行的最小大小的证明，并将通过尝试识别证书的形式和优化此类证书的大小来探索认证问题。

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.