Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL
Ralph Bottesch, Maximilian P. L. Haslbeck, René Thiemann · Lecture notes in computer science · 2019
Dutertre and de Moura developed a simplex-based solver for linear rational arithmetic that has an incremental interface and provides unsatisfiable cores. We present a verification of their algorithm in Isabelle/HOL that significantly extends previous work by Spasić and Marić. Based on the simplex algorithm we further formalize Farkas’ Lemma. With this result we verify that linear rational constraints are satisfiable over $$\mathbb {Q}$$ if and only they are satisfiable over $$\mathbb {R}$$ . Hence, our verified simplex algorithm is also able to decide satisfiability in linear real arithmetic.