Correctness of results from mixed-integer linear programming (MILP) solvers is critical, particularly in the context of applications such as hardware verification, compiler optimization, or machine-assisted theorem proving. To this end, VIPR 1.0 is the first recently proposed general certificate format for answers produced by MILP solvers. We design a schema to encode VIPR's inference rules as a ground formula that completely characterizes the validity of the algorithmic check, removing any ambiguities and imprecisions present in the specification. We formally verify the correctness of our schema at the logical level using Why3's automated deductive logic framework. Furthermore, we implement a checker for VIPR certificates by expressing our formally verified ground formula with the Satisfiability Modulo Theory Library (SMT-LIB) and check its validity. Our approach is solver-agnostic, and we test its viability using benchmark instances found in the literature.

翻译：混合整数线性规划（MILP）求解器结果的正确性至关重要，特别是在硬件验证、编译器优化或机器辅助定理证明等应用背景下。为此，VIPR 1.0是最近首次提出的用于MILP求解器所产生答案的通用证书格式。我们设计了一种方案，将VIPR的推理规则编码为一个完全刻画算法检查有效性的基公式，消除了规范中存在的任何模糊性和不精确之处。我们使用Why3的自动演绎逻辑框架，在逻辑层面形式化地验证了我们方案的正确性。此外，我们通过用可满足性模理论库（SMT-LIB）表达我们形式化验证的基公式，实现了一个VIPR证书检查器，并验证其有效性。我们的方法与求解器无关，并使用文献中的基准实例测试了其可行性。