Constraint solving is an integral part of program verification, in general and abstract interpretation in particular. This proposal explores some 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.
