@inproceedings{WST10,
  author    = {Ren\'e Thiemann and Christian Sternagel},
  title     = {Certified Polynomial Interpretations over Matrices and over Domains}, 
  year      = 2010,
  booktitle = {Proc.\ WST '10},
  note = "To appear."
}

@Article{MatrixJAR,
  author =       {J.~Endrullis and J.~Waldmann and H.~Zantema},
  title =        {{Matrix Interpretations for Proving Termination of Term Rewriting}},
  journal =      {Journal of Automated Reasoning},
  year =         {2008},
  OPTkey =       {},
  volume =       {40},
  number =       {2-3},
  pages =        {195--220},
  OPTmonth =     {},
  OPTnote =      {},
  OPTannote =    {}
}

@inproceedings{Arctic,
  author    = {A.\ Koprowski and J.\ Waldmann},
  title     = {Arctic Termination {\ldots} Below Zero},
  booktitle = {Proc.\ RTA'08},
  year      = {2008},
  pages     = {202--216},
  series = "LNCS 5117"
}

@inproceedings{CeTA,
  author    = {R.~Thiemann and C.~Sternagel},
  title     = {Certification of Termination Proofs using \ceta},
  booktitle = {Proc.\ TPHOLs'09},
  series    = {LNCS 5674},
  year      = 2009,
  pages     = {452--468}
}
@inproceedings{CeTAcomplexity,
  author    = {M.~Avanzini and C.~Sternagel and R.~Thiemann},
  title     = {Certification of Complexity Proofs using \ceta},
  booktitle = {Proc.\ {RTA} 2015},
  series    = {LIPIcs 36},
  pages     = {23--39},
  year      = {2015}
}

@book{PO07,
  title={Matrix theory: from generalized inverses to {J}ordan form},
  author={Piziak, Robert and Odell, Patrick L},
  year={2007},
  publisher={CRC Press}
}

@article{Containers-AFP,
  author  = {Andreas Lochbihler},
  title   = {Light-weight Containers},
  journal = {Archive of Formal Proofs},
  month   = apr,
  year    = 2013,
  note    = {\url{http://isa-afp.org/entries/Containers.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Gauss_Jordan-AFP,
  author  = {Jose Divas\'on and Jesus Aransay},
  title   = {Gauss-Jordan Algorithm and Its Applications},
  journal = {Archive of Formal Proofs},
  month   = sep,
  year    = 2014,
  note    = {\url{http://isa-afp.org/entries/Gauss_Jordan.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@article{Matrix-AFP,
  author  = {Christian Sternagel and Rene Thiemann},
  title   = {Executable Matrix Operations on Matrices of Arbitrary Dimensions},
  journal = {Archive of Formal Proofs},
  month   = jun,
  year    = 2010,
  note    = {\url{http://isa-afp.org/entries/Matrix.shtml},
            Formal proof development},
  ISSN    = {2150-914x},
}

@book{schrijver1998theory,
  title={Theory of linear and integer programming},
  author={Schrijver, Alexander},
  year={1998},
  publisher={John Wiley \& Sons}
}

@inproceedings{incremental_simplex,
  author    = {Bruno Dutertre and
               Leonardo Mendon{\c{c}}a de Moura},
  opteditor    = {Thomas Ball and
               Robert B. Jones},
  title     = {A Fast Linear-Arithmetic Solver for {DPLL(T)}},
  booktitle = {Proc. Computer Aided Verification}, 
  series    = {LNCS},
  volume    = {4144},
  pages     = {81--94},
  publisher = {Springer},
  year      = {2006},
  note      = {Extended version available as Technical Report, CSL-06-01, SRI International.},
  doi       = {10.1007/11817963\_11},
}

@article{Papad,
  author    = {Christos H. Papadimitriou},
  title     = {On the complexity of integer programming},
  journal   = {J. {ACM}},
  volume    = {28},
  number    = {4},
  pages     = {765--768},
  year      = {1981},
  url       = {https://doi.org/10.1145/322276.322287},
  doi       = {10.1145/322276.322287},
}
