@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}
}
