@inproceedings{SpasicMaric,
        Author = {Mirko Spasi\'c and Filip Mari\'c},
        Booktitle = {FM'12},
        Doi = {10.1007/978-3-642-32759-9_35},
        Editor = {Dimitra Giannakopoulou and Dominique M{\'{e}}ry},
        Opt_Publisher = {Springer},
        Series = {LNCS},
        Volume = {7436},
        Year = {2012},
        Pages = {434--449},
        Title = {Formalization of Incremental Simplex Algorithm by Stepwise Refinement},
        Bdsk-Url-1 = {http://dx.doi.org/10.1007/978-3-642-32759-9_35}}


@inproceedings{florian-refinement,
        Author = {Florian Haftmann and Alexander Krauss and Ondrej Kun\v{c}ar and Tobias Nipkow},
        Booktitle = {ITP'13},
        Optpublisher = {Springer},
        editor    = {Sandrine Blazy and
               Christine Paulin{-}Mohring and
               David Pichardie},
        Pages = {100--115},
        Series = {LNCS},
        Title = {Data Refinement in {I}sabelle/{HOL}},
        Volume = {7998},
        Year = {2013}}

@inproceedings{simplex-rad, 
        author    = {Bruno Dutertre and Leonardo Mendon\c{c}a de Moura},
        editor    = {Thomas Ball and Robert B. Jones},
        title     = {A Fast Linear-Arithmetic Solver for {DPLL(T)}},
        booktitle = {CAV'06}, 
        series    = {LNCS},
        volume    = {4144},
        pages     = {81--94},
        optpublisher = {Springer},
        year      = {2006},
        doi       = {10.1007/11817963_11},
}

@book{LinearProgramming,
	Author = {Alexander Schrijver},
	Publisher = {Wiley},
	Title = {Theory of linear and integer programming},
	Year = {1999}
}

@book{StoerWitzgall,
        title =     {Convexity and Optimization in Finite Dimensions I},
        author =    {Josef Stoer and Christoph Witzgall},
        publisher = {Springer-Verlag Berlin Heidelberg},
        isbn =      {978-3-642-46218-4,978-3-642-46216-0},
        year =      {1970},
        series =    {Die Grundlehren der mathematischen Wissenschaften 163},
        edition =   {1},
        volume =    {},
}

@Article{Bromberger2017,
         author="Martin Bromberger and Christoph Weidenbach",
         title="New techniques for linear arithmetic: cubes and equalities",
         journal="Formal Methods in System Design",
         year="2017",
         month="Dec",
         day="01",
         volume="51",
         number="3",
         pages="433--461",
         issn="1572-8102",
         doi="10.1007/s10703-017-0278-7",
         url="https://doi.org/10.1007/s10703-017-0278-7"
}

@article{simplex-afp,
  author  = {Filip Mari\'c and Mirko Spasi\'c and Ren\'e Thiemann},
  title   = {An Incremental Simplex Algorithm with Unsatisfiable Core Generation},
  journal = {Archive of Formal Proofs},
  month   = aug,
  year    = 2018,
  note    = {\url{http://isa-afp.org/entries/Simplex.html},
            Formal proof development},
  ISSN    = {2150-914x},
}

@inproceedings{Thiemann18,
  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}
}
