Chevillard, S.; Harrison, J.; Joldeş, M.; Lauter, Ch. Efficient and accurate computation of upper bounds of approximation errors. (English) Zbl 1211.65025 Theor. Comput. Sci. 412, No. 16, 1523-1543 (2011). MSC: 65D20 26A09 33B10 65G20 33F05 PDFBibTeX XMLCite \textit{S. Chevillard} et al., Theor. Comput. Sci. 412, No. 16, 1523--1543 (2011; Zbl 1211.65025) Full Text: DOI Link
Cornea, Marius; Harrison, John; Anderson, Cristina; Tang, Ping Tak Peter; Schneider, Eric; Gvozdev, Evgeny A software implementation of the IEEE 754R decimal floating-point arithmetic using the binary encoding format. (English) Zbl 1367.65212 IEEE Trans. Comput. 58, No. 2, 148-162 (2009). MSC: 65Y04 PDFBibTeX XMLCite \textit{M. Cornea} et al., IEEE Trans. Comput. 58, No. 2, 148--162 (2009; Zbl 1367.65212) Full Text: DOI
Harrison, John Floating-point verification using theorem proving. (English) Zbl 1182.68120 Bernardo, Marco (ed.) et al., Formal methods for hardware verification. 6th international school on formal methods for the design of computer, communication, and software systems, SFM 2006, Bertinoro, Italy, May 22–27, 2006. Advanced lectures. Berlin: Springer (ISBN 3-540-34304-0/pbk). Lecture Notes in Computer Science 3965, 211-242 (2006). MSC: 68Q60 65Y04 68M07 68T15 PDFBibTeX XMLCite \textit{J. Harrison}, Lect. Notes Comput. Sci. 3965, 211--242 (2006; Zbl 1182.68120) Full Text: DOI
Harrison, John Formal verification of IA-64 division algorithms. (English) Zbl 0974.68535 Aagaard, Mark (ed.) et al., Theorem proving in higher order logics. 13th international conference, TPHOLs 2000, Portland, OR, USA, August 14-18, 2000. Proceedings. Berlin: Springer. Lect. Notes Comput. Sci. 1869, 233-251 (2000). MSC: 68T15 65Y10 65G50 PDFBibTeX XMLCite \textit{J. Harrison}, Lect. Notes Comput. Sci. 1869, 233--251 (2000; Zbl 0974.68535)