Abstract

As an ingredient for a verified DPLL solver, it is crucial to have a theory solver that has an incremental interface and provides unsatisfiable cores. To this end, we extend the Isabelle/HOL formalization of the simplex algorithm by Spasic and Maric. We further discuss the impact of their design decisions on the development of our extension.

BibTeX

@inproceedings{RT-IWIL2018,
  author    = {Ren\'e Thiemann},
  title     = {Extending a Verified Simplex Algorithm},
  booktitle = {LPAR-22 Workshop and Short Paper Proceedings},
  editor    = {Gilles Barthe and Konstantin Korovin and 
               Stephan Schulz and Martin Suda and 
               Geoff Sutcliffe and Margus Veanes},
  series    = {Kalpa Publications in Computing},
  volume    = {9},
  pages     = {37--48},
  year      = {2018},
  publisher = {EasyChair},
  doi       = {10.29007/5vlq}
}