Abstract

We implement a decision procedure for linear mixed integer arithmetic and formally verify its soundness in Isabelle/HOL. We further integrate this procedure into one application, namely into CeTA, a formally verified certifier to check untrusted termination proofs. This checking involves assertions of unsatisfiability of linear integer inequalities; previously, only a sufficient criterion for such checks was supported. To verify the soundness of the decision procedure, we first formalize the proof that every satisfiable set of linear integer inequalities also has a small solution, and give explicit upper bounds. To this end we mechanize several important theorems on linear programming, including statements on integrality and bounds. The procedure itself is then implemented as a branch-and-bound algorithm, and is available in several languages via Isabelle’s code generator. It internally relies upon an adapted version of an existing verified incremental simplex algorithm.

BibTeX

@inproceedings{RBMHARRT20,
  author    = {Ralph Bottesch and
               Max W. Haslbeck and
               Alban Reynaud and
               Ren\'e Thiemann},
  editor    = {Ritchie Lee and
               Susmit Jha and
               Anastasia Mavridou},
  title     = {Verifying a Solver for Linear Mixed Integer Arithmetic in {I}sabelle/{HOL}},
  booktitle = {12th International NASA Formal Methods Symposium (NFM 2020)},
  series    = {LNCS},
  volume    = {12229},
  pages     = {233--250},
  publisher = {Springer},
  year      = {2020},
  doi       = {10.1007/978-3-030-55754-6_14}
}