Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle/HOL

被引：0

作者：

Bottesch, Ralph ^{[1
]}

Haslbeck, Max W. ^{[1
]}

Reynaud, Alban ^{[2
]}

Thiemann, Rene ^{[1
]}

机构：

[1] Univ Innsbruck, Innsbruck, Austria

[2] ENS Lyon, Lyon, France

来源：

NASA FORMAL METHODS (NFM 2020) | 2020年 / 12229卷

基金：

奥地利科学基金会;

关键词：

Branch-and-bound; Isabelle/HOL; Linear programming; Polyhedra; Simplex algorithm;

D O I：

10.1007/978-3-030-55754-6_26

中图分类号：

TP39 [计算机的应用];

学科分类号：

081203 ; 0835 ;

摘要：

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.

引用

页码：233 / 250

页数：18

共 24 条

[1] A Formalization of Convex Polyhedra Based on the Simplex Method
Allamigeon, Xavier
Katz, Ricardo D.
[J]. INTERACTIVE THEOREM PROVING (ITP 2017), 2017, 10499 : 28 - 45
[2] [Anonymous], 1999, WILEY INTERSCIENCE S
[3] [Anonymous], 2017, LNCS LNAI, V10395, P454, DOI [10.1007/978-3-319-63046-528, DOI 10.1007/978-3-319-63046-528]
[4] Barrett Clark, 2011, Computer Aided Verification. Proceedings 23rd International Conference, CAV 2011, P171, DOI 10.1007/978-3-642-22110-1_14
[5] Bottesch R., 2019, LINEAR INEQUALITIES
[6] Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL
Bottesch, Ralph
Haslbeck, Max W.
Thiemann, Rene
[J]. FRONTIERS OF COMBINING SYSTEMS (FROCOS 2019), 2019, 11715 : 223 - 239
[7] Brockschmidt M., CADE
[8] Bromberger M., REDUCTION UNBOUNDED
[9] Carlier Matthieu, 2012, FM 2012: Formal Methods. Proceedings of the 18th International Symposium, P116, DOI 10.1007/978-3-642-32759-9_12
[10] Dantzig G., 1963, LINEAR PROGRAMMING E, DOI [DOI 10.1515/9781400884179, 10.7249/R366, DOI 10.7249/R366]

← 1 2 3 →