benchmarks.bib

@article{damouche-martel-chapoutot-fmics15,
  author="Damouche, Nasrine and Martel, Matthieu and Chapoutot, Alexandre",
  editor="N{\'u}{\~{n}}ez, Manuel and G{\"u}demann, Matthias",
  chapter="Intra-procedural Optimization of the Numerical Accuracy of Programs",
  title="Formal Methods for Industrial Critical Systems: 20th International Workshop, FMICS 2015 Oslo, Norway, June 22-23, 2015 Proceedings",
  year="2015",
  publisher="Springer International Publishing",
  address="Cham",
  pages="31--46",
  isbn="978-3-319-19458-5",
  doi="10.1007/978-3-319-19458-5_3",
  url="http://dx.doi.org/10.1007/978-3-319-19458-5_3"
}

@article{damouche-martel-chapoutot-nsv14,
  title = "Transformation of a \{PID\} Controller for Numerical Accuracy ",
  journal = "Electronic Notes in Theoretical Computer Science ",
  volume = "317",
  number = "",
  pages = "47 - 54",
  year = "2015",
  note = "The Seventh and Eighth International Workshops on Numerical Software Verification (NSV) ",
  issn = "1571-0661",
  doi = "http://dx.doi.org/10.1016/j.entcs.2015.10.006",
  url = "http://www.sciencedirect.com/science/article/pii/S157106611500047X",
  author = "N. Damouche and M. Martel and A. Chapoutot",
  keywords = "Numerical Accuracy",
  keywords = "Semantics-Based Program Transformation",
  keywords = "Floating-Point Arithmetic",
  keywords = "Validation of Numerical Programs "
}

@article{feron-ieee10,
  author={E. Feron},
  journal={IEEE Control Systems},
  title={From Control Systems to Control Software},
  year={2010},
  volume={30},
  number={6},
  pages={50-71},
  keywords={Lyapunov methods;control engineering computing;formal specification;stability;theorem proving;Floyd-Hoare paradigm;Lyapunov-theoretic proof;Simulink;control program code;control program documentation;control software;control system;control theory;diagram-based specification;formally annotated target code;logical expression;proof checker;reachable program state;stability;Human factors;Safety;Software;Stability;Closed-loop stability;Control software},
  doi={10.1109/MCS.2010.938196},
  ISSN={1066-033X},
  month={Dec},
}

@inproceedings{damouche-martel-chapoutot-cf15,
  author = {Damouche, Nasrine and Martel, Matthieu and Chapoutot, Alexandre},
  title = {Optimizing the Accuracy of a Rocket Trajectory Simulation by Program Transformation},
  booktitle = {Proceedings of the 12th ACM International Conference on Computing Frontiers},
  series = {CF '15},
  year = {2015},
  isbn = {978-1-4503-3358-0},
  location = {Ischia, Italy},
  pages = {40:1--40:2},
  articleno = {40},
  numpages = {2},
  url = {http://doi.acm.org/10.1145/2742854.2742894},
  doi = {10.1145/2742854.2742894},
  acmid = {2742894},
  publisher = {ACM},
  address = {New York, NY, USA},
  keywords = {abstract interpretation, accuracy, compiler optimizations, floating-point numbers, program transformation},
} 

@book{atkinson-1989,
  title={An Introduction to Numerical Analysis},
  author={Atkinson, K.},
  isbn={9780471624899},
  lccn={88000718},
  url={https://books.google.com/books?id=cMLsbz0X6oIC},
  year={1989},
  publisher={Wiley}
}

@book{golub-vanloan-1996,
  author = {Golub, Gene H. and Van Loan, Charles F.},
  title = {Matrix Computations (3rd Ed.)},
  year = {1996},
  isbn = {0-8018-5414-8},
  publisher = {Johns Hopkins University Press},
  address = {Baltimore, MD, USA},
} 

@article{abdelmalek-bit71,
  author="Abdelmalek, Nabih N.",
  title="Round off error analysis for Gram-Schmidt method and solution of linear least squares problems",
  journal="BIT Numerical Mathematics",
  volume="11",
  number="4",
  pages="345--367",
  issn="1572-9125",
  doi="10.1007/BF01939404",
  url="http://dx.doi.org/10.1007/BF01939404"
}

@techreport{hernandez-roman-tomas-vidal-tr07,
  author      = "V. Hernandez and J. E. Roman and A. Tomas and V. Vidal",
  title       = "A survey of software for sparse eigenvalue problems",
  number      = "STR-6",
  institution = "Universitat Polit\`ecnica de Val\`encia",
  note        = "Available at http://slepc.upv.es",
  year        = "2009"
}

@book{hamming-1987,
  title = {Numerical Methods for Scientists and Engineers},
  author = {Richard Hamming},
  publisher = {Dover Publications},
  year = {1987},
  edition = {2nd},
}

@inproceedings{darulova-kuncak-2014,
 author = {Darulova, Eva and Kuncak, Viktor},
 title = {Sound Compilation of Reals},
 series = {POPL '14},
 year = {2014},
 isbn = {978-1-4503-2544-8},
 location = {San Diego, California, USA},
 pages = {235--248},
 numpages = {14},
 url = {http://doi.acm.org/10.1145/2535838.2535874},
 acmid = {2535874},
 publisher = {ACM},
 address = {New York, NY, USA},
 keywords = {compilation, embedded systems, fixed-point arithmetic, floating-point arithmetic, numerical approximation, roundoff error, scientific computing, sensitivity analysis, verification},
} 

@inproceedings{solovyev-et-al-2015,
  author = {Alexey Solovyev and Charlie Jacobsen and Zvonimir Rakamaric and Ganesh Gopalakrishnan},
  title = {Rigorous Estimation of Floating-Point Round-off Errors with Symbolic Taylor Expansions},
  doi = {10.1007/978-3-319-19249-9_33},
  url = {https://link.springer.com/chapter/10.1007/978-3-319-19249-9_33},
  series = {FM'15},
  publisher = {Springer},
  year = {2015},
  month = jun,
}

@inproceedings{herbie-2015,
  author    = {P. Panchekha,
               A. Sanchez{-}Stern,
               J.-R. Wilcox and
               Z. Tatlock},
  title     = {Automatically improving accuracy for floating point expressions},
  booktitle = {PLDI'15},
  pages     = {1--11},
  editor    = {D. Grove and
               S. Blackburn},
  publisher = {{ACM}},
  url = {http://doi.acm.org/10.1145/2813885.2737959},
  doi = {10.1145/2813885.2737959},
  year      = {2015},
}

@inproceedings{precimonious-2013,
  title = {Precimonious: Tuning assistant for floating-point precision},
  author = {Rubio-Gonz{\'a}lez, Cindy and Nguyen, Cuong and Nguyen, Hong Diep and Demmel, James and Kahan, William and Sen, Koushik and Bailey, David H and Iancu, Costin and Hough, David},
  booktitle = {High Performance Computing, Networking, Storage and Analysis (SC), 2013 International Conference for},
  pages = {1--12},
  year = {2013},
  organization = {IEEE}
  url = {http://doi.acm.org/10.1145/2503210.2503296},
  doi = {10.1145/2503210.2503296},
}

@article{rump-revisited-2002,
author = {Loh, Eugene and Walster, G. William},
year = {2002},
month = {01},
pages = {245-248},
title = {Rump's Example Revisited},
volume = {8},
journal = {Reliable Computing},
doi = {10.1023/A:1015569431383}
}

@InProceedings{adje-2010,
  author="Adj{\'e}, Assal{\'e} and Gaubert, St{\'e}phane and Goubault, Eric",
  editor="Gordon, Andrew D.",
  title="Coupling Policy Iteration with Semi-definite Relaxation to Compute Accurate Numerical Invariants in Static Analysis",
  booktitle="Programming Languages and Systems",
  year="2010",
  publisher="Springer Berlin Heidelberg",
  address="Berlin, Heidelberg",
  pages="23--42",
  isbn="978-3-642-11957-6"
}

@PHDTHESIS{bibek-2020,
url = "http://www.theses.fr/2020IPPAX017",
title = "Synthesizing invariants : a constraint programming approach based on zonotopic abstraction",
author = "Kabi, Bibek",
year = "2020",
note = "Thèse de doctorat dirigée par Putot, Sylvie Informatique, données, IA Institut polytechnique de Paris 2020",
note = "2020IPPAX017",
url = "http://www.theses.fr/2020IPPAX017/document",
}