Abstract

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 Q if and only they are satisfiable over R. Hence, our verified simplex algorithm is also able to decide satisfiability in linear real arithmetic.

BibTeX

@inproceedings{RBMHRT-FROCOS19,
  author    = "Ralph Bottesch and Max W. Haslbeck and René Thiemann",
  title     = "Verifying an Incremental Theory Solver for Linear Arithmetic in Isabelle/HOL",
  booktitle = "Proceedings of the 12th International Symposium on Frontiers of Combining Systems", 
  editor    = "A. Herzig and A. Popescu",
  series    = "Lecture Notes in Computer Science",
  volume    = 11715,
  pages     = "223--239",
  year      = 2019,
  doi       = "10.1007/978-3-030-29007-8_13"
}