Ralph Bottesch, Max W. Haslbeck, Alban Reynaud, René Thiemann
12th International NASA Formal Methods Symposium (NFM 2020), LNCS 12229, pp. 233 – 250, 2020.
doi:10.1007/978-3-030-55754-6_14 AFP entry
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}}