{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,30]],"date-time":"2025-12-30T23:24:54Z","timestamp":1767137094450,"version":"build-2238731810"},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030557539","type":"print"},{"value":"9783030557546","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>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 , 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\u2019s code generator. It internally relies upon an adapted version of an existing verified incremental simplex algorithm.<\/jats:p>","DOI":"10.1007\/978-3-030-55754-6_14","type":"book-chapter","created":{"date-parts":[[2020,8,9]],"date-time":"2020-08-09T19:02:37Z","timestamp":1596999757000},"page":"233-250","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Verifying a Solver for Linear Mixed Integer Arithmetic in Isabelle\/HOL"],"prefix":"10.1007","author":[{"given":"Ralph","family":"Bottesch","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-9900-5746","authenticated-orcid":false,"given":"Max W.","family":"Haslbeck","sequence":"additional","affiliation":[]},{"given":"Alban","family":"Reynaud","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0323-8829","authenticated-orcid":false,"given":"Ren\u00e9","family":"Thiemann","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,8,10]]},"reference":[{"key":"14_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-319-66107-0_3","volume-title":"Interactive Theorem Proving","author":"X Allamigeon","year":"2017","unstructured":"Allamigeon, X., Katz, R.D.: A formalization of convex polyhedra based on the simplex method. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) ITP 2017. LNCS, vol. 10499, pp. 28\u201345. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-66107-0_3"},{"key":"14_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1007\/978-3-642-22110-1_14","volume-title":"Computer Aided Verification","author":"C Barrett","year":"2011","unstructured":"Barrett, C., et al.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171\u2013177. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_14"},{"key":"14_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/978-3-030-29007-8_13","volume-title":"Frontiers of Combining Systems","author":"R Bottesch","year":"2019","unstructured":"Bottesch, R., Haslbeck, M.W., Thiemann, R.: Verifying an incremental theory solver for linear arithmetic in Isabelle\/HOL. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 223\u2013239. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_13"},{"key":"14_CR4","unstructured":"Bottesch, R., Reynaud, A., Thiemann, R.: Linear inequalities. Archive of Formal Proofs, June 2019. http:\/\/isa-afp.org\/entries\/Linear_Inequalities.html. Formal proof development"},{"key":"14_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"454","DOI":"10.1007\/978-3-319-63046-5_28","volume-title":"Automated Deduction \u2013 CADE 26","author":"M Brockschmidt","year":"2017","unstructured":"Brockschmidt, M., Joosten, S.J.C., Thiemann, R., Yamada, A.: Certifying safety and termination proofs for integer transition systems. In: de Moura, L. (ed.) CADE 2017. LNCS (LNAI), vol. 10395, pp. 454\u2013471. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63046-5_28"},{"key":"14_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/978-3-319-94205-6_22","volume-title":"Automated Reasoning","author":"M Bromberger","year":"2018","unstructured":"Bromberger, M.: A reduction from unbounded linear mixed arithmetic problems into bounded problems. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 329\u2013345. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_22"},{"issue":"3","key":"14_CR7","doi-asserted-by":"publisher","first-page":"433","DOI":"10.1007\/s10703-017-0278-7","volume":"51","author":"M Bromberger","year":"2017","unstructured":"Bromberger, M., Weidenbach, C.: New techniques for linear arithmetic: cubes and equalities. Form. Methods Syst. Des. 51(3), 433\u2013461 (2017). https:\/\/doi.org\/10.1007\/s10703-017-0278-7","journal-title":"Form. Methods Syst. Des."},{"key":"14_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1007\/978-3-642-32759-9_12","volume-title":"FM 2012: Formal Methods","author":"M Carlier","year":"2012","unstructured":"Carlier, M., Dubois, C., Gotlieb, A.: A certified constraint solver over finite domains. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 116\u2013131. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_12"},{"key":"14_CR9","doi-asserted-by":"publisher","DOI":"10.7249\/R366","volume-title":"Linear Programming and Extensions","author":"GB Dantzig","year":"1963","unstructured":"Dantzig, G.B.: Linear Programming and Extensions. Princeton University Press, Princeton (1963)"},{"key":"14_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"81","DOI":"10.1007\/11817963_11","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2006","unstructured":"Dutertre, B., de Moura, L.: A fast linear-arithmetic solver for DPLL(T). In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 81\u201394. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11817963_11"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103\u2013117. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-12251-4_9"},{"key":"14_CR12","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-012-9250-9","volume":"50","author":"J Harrison","year":"2013","unstructured":"Harrison, J.: The HOL light theory of Euclidean space. J. Autom. Reasoning 50, 173\u2013190 (2013). https:\/\/doi.org\/10.1007\/s10817-012-9250-9","journal-title":"J. Autom. Reasoning"},{"issue":"4","key":"14_CR13","doi-asserted-by":"publisher","first-page":"303","DOI":"10.1007\/s10817-009-9157-2","volume":"44","author":"A Krauss","year":"2010","unstructured":"Krauss, A.: Partial and nested recursive function definitions in higher-order logic. J. Autom. Reasoning 44(4), 303\u2013336 (2010). https:\/\/doi.org\/10.1007\/s10817-009-9157-2","journal-title":"J. Autom. Reasoning"},{"issue":"1\u20133","key":"14_CR14","doi-asserted-by":"publisher","first-page":"397","DOI":"10.1016\/S0166-218X(01)00348-1","volume":"123","author":"H Marchand","year":"2002","unstructured":"Marchand, H., Martin, A., Weismantel, R., Wolsey, L.A.: Cutting planes in integer and mixed integer programming. Discrete Appl. Math. 123(1\u20133), 397\u2013446 (2002). https:\/\/doi.org\/10.1016\/S0166-218X(01)00348-1","journal-title":"Discrete Appl. Math."},{"key":"14_CR15","unstructured":"Mari\u0107, F., Spasi\u0107, M., Thiemann, R.: An incremental simplex algorithm with unsatisfiable core generation. Archive of Formal Proofs, August 2018. http:\/\/isa-afp.org\/entries\/Simplex.html. Formal proof development"},{"key":"14_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"14_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"326","DOI":"10.1007\/978-3-642-54108-7_17","volume-title":"Verified Software: Theories, Tools, Experiments","author":"A Narkawicz","year":"2014","unstructured":"Narkawicz, A., Mu\u00f1oz, C.: A formally verified generic branching algorithm for global optimization. In: Cohen, E., Rybalchenko, A. (eds.) VSTTE 2013. LNCS, vol. 8164, pp. 326\u2013343. Springer, Heidelberg (2014). https:\/\/doi.org\/10.1007\/978-3-642-54108-7_17"},{"issue":"2","key":"14_CR18","doi-asserted-by":"publisher","first-page":"189","DOI":"10.1007\/s10817-010-9183-0","volume":"45","author":"T Nipkow","year":"2010","unstructured":"Nipkow, T.: Linear quantifier elimination. J. Autom. Reasoning 45(2), 189\u2013212 (2010). https:\/\/doi.org\/10.1007\/s10817-010-9183-0","journal-title":"J. Autom. Reasoning"},{"key":"14_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL \u2013 A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"4","key":"14_CR20","doi-asserted-by":"publisher","first-page":"765","DOI":"10.1145\/322276.322287","volume":"28","author":"CH Papadimitriou","year":"1981","unstructured":"Papadimitriou, C.H.: On the complexity of integer programming. J. ACM 28(4), 765\u2013768 (1981). https:\/\/doi.org\/10.1145\/322276.322287","journal-title":"J. ACM"},{"key":"14_CR21","volume-title":"Theory of Linear and Integer Programming","author":"A Schrijver","year":"1999","unstructured":"Schrijver, A.: Theory of Linear and Integer Programming. Wiley, Hoboken (1999)"},{"key":"14_CR22","doi-asserted-by":"publisher","unstructured":"Smith, A., Mu\u00f1oz, C., Narkawicz, A., Markevicius, M.: A rigorous generic branch and bound solver for nonlinear problems. In: 2015 17th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing (SYNASC), pp. 71\u201378. IEEE (2015). https:\/\/doi.org\/10.1109\/SYNASC.2015.20","DOI":"10.1109\/SYNASC.2015.20"},{"key":"14_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"434","DOI":"10.1007\/978-3-642-32759-9_35","volume-title":"FM 2012: Formal Methods","author":"M Spasi\u0107","year":"2012","unstructured":"Spasi\u0107, M., Mari\u0107, F.: Formalization of incremental simplex algorithm by stepwise refinement. In: Giannakopoulou, D., M\u00e9ry, D. (eds.) FM 2012. LNCS, vol. 7436, pp. 434\u2013449. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-32759-9_35"},{"key":"14_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"452","DOI":"10.1007\/978-3-642-03359-9_31","volume-title":"Theorem Proving in Higher Order Logics","author":"R Thiemann","year":"2009","unstructured":"Thiemann, R., Sternagel, C.: Certification of termination proofs using CeTA. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol. 5674, pp. 452\u2013468. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-03359-9_31"}],"updated-by":[{"DOI":"10.1007\/978-3-030-55754-6_26","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2020,8,10]],"date-time":"2020-08-10T00:00:00Z","timestamp":1597017600000}}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-55754-6_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,1]],"date-time":"2020-12-01T08:53:21Z","timestamp":1606812801000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-55754-6_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030557539","9783030557546"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-55754-6_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"10 August 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"10 August 2020","order":2,"name":"change_date","label":"Change Date","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Correction","order":3,"name":"change_type","label":"Change Type","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The original versions of this book and Chapter 14 were revised. The following was corrected:","order":4,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Dimitra Giannakopoulou, the General Chair of the NFM 2020 conference, was inadvertently forgotten and, therefore, added as a volume editor.","order":5,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"Chapter 14 was retrospectively made available open access under a CC BY 4.0 license at link.springer.com.","order":6,"name":"change_details","label":"Change Details","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"NFM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"NASA Formal Methods Symposium","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Moffett Field, CA","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"USA","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 May 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 May 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"nfm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ti.arc.nasa.gov\/events\/nfm-2020\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"62","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"20","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"5","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"32% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"4.5","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}