Extending a Verified Simplex Algorithm

René Thiemann

13th International Workshop on the Implementation of Logics, Kalpa Publications in Computing 9, pp. 37 – 48, 2018.


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.


  PDF |    doi:10.29007/5vlq


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}
Nach oben scrollen