High-Level Verification Using Theorem Proving and Formalized Mathematics

1. Bailey, D., Borwein, P., Plouffe, S.: On the rapid computation of various poly- logarithmic constants. Mathematics of Computation 66, 903–913 (1997)

   Article  MATH  MathSciNet  Google Scholar 

2. Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.): TPHOLs 1999. LNCS, vol. 1690, p. 83. Springer, Heidelberg (1999)

   MATH  Google Scholar 

3. Boulton, R.J.: Effciency in a fully-expansive theorem prover. Technical Report 337, University of Cambridge Computer Laboratory, New Museums Site, Pembroke Street, Cambridge, CB2 3QG, UK, Author’s PhD thesis (1993)

   Google Scholar 

4. Cousineau, G., Mauny, M.: The Functional Approach to Programming. Cambridge University Press, Cambridge (1998)

   MATH  Google Scholar 

5. Gordon, M.J.C., Melham, T.F.: Introduction to HOL: a theorem proving environment for higher order logic. Cambridge University Press, Cambridge (1993)

   MATH  Google Scholar 

6. Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF. LNCS, vol. 78. Springer, Heidelberg (1979)

   MATH  Google Scholar 

7. Harrison, J.: Metatheory and reflection in theorem proving: A survey and critique. Technical Report CRC-053, SRI Cambridge, Millers Yard, Cambridge, UK (1995), Available on the Web as, http://www.cl.cam.ac.uk/users/jrh/papers/reflect.dvi.gz

8. Harrison, J.: HOL Light: A tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265–269. Springer, Heidelberg (1996)

   Chapter  Google Scholar 

9. Harrison, J.: A Mizar mode for HOL. In: von Wright, J., Harrison, J., Grundy, J. (eds.) TPHOLs 1996. LNCS, vol. 1125, pp. 203–220. Springer, Heidelberg (1996)

   Google Scholar 

10. Harrison, J.: Proof style. In: Giménez, E. (ed.) TYPES 1996. LNCS, vol. 1512, pp. 154–172. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

11. Harrison, J.: Theorem Proving with the Real Numbers. Springer-Verlag (1998), Revised version of author’s PhD thesis

    Google Scholar 

12. Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot et al. [2], pp. 113–130

    Google Scholar 

13. IEEE. Standard for binary floating point arithmetic. ANSI/IEEE Standard 754- 1985, The Institute of Electrical and Electronic Engineers, Inc., 345 East 47th Street, New York, NY 10017, USA (1985)

    Google Scholar 

14. Knopp, K.: Theory and Application of Infinite Series, 2nd edn. Blackie and Son Ltd. (1951)

    Google Scholar 

15. Kumar, R., Kropf, T., Schneider, K.: Integrating a first-order automatic prover in the HOL environment. In: Archer, M., Joyce, J.J., Levitt, K.N. (eds.) Proceedings of the 1991 International Workshop on the HOL theorem proving system and its Applications, University of California at Davis, Davis CA, USA, pp. 170–176. IEEE Computer Society Press, Los Alamitos (1991)

    Chapter  Google Scholar 

16. Moore, J.S., Lynch, T., Kaufmann, M.: A mechanically checked proof of the correctness of the kernel of the AMD5_K86 floating-point division program. IEEE Transactions on Computers 47, 913–926 (1998)

    Article  MathSciNet  Google Scholar 

17. O’Leary, J., Zhao, X., Gerth, R., Seger, C.-J.H.: Formally verifying IEEE compliance of floating-point hardware. Intel Technology Journal 1999-Q1, 1–14 (1999), Available on the Web as http://developer.intel.com/technology/itj/q11999/articles/art_5.htm.

18. Rudnicki, P.: An overview of the MIZAR project. Available on the Web as http://web.cs.ualberta.ca/~piotr/Mizar/MizarOverview.ps (1992)

19. Rusinoff, D.: A mechanically checked proof of IEEE compliance of a register-transfer-level specification of the AMD-K7 floating-point multiplication, division, and square root instructions. LMS Journal of Computation and Mathematics 1, 148–200 (1998), Available on the Web via http://www.onr.com/user/russ/david/k7-div-sqrt.html

    Google Scholar 

20. Russell, B.: The autobiography of Bertrand Russell. Allen & Unwin (1968)

    Google Scholar 

21. Syme, D.: Three tactic theorem proving. In: Bertot et al. [2], pp. 203–220

    Google Scholar 

22. Trybulec, A.: The Mizar-QC/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing) 6, 136–140 (1978)

    Google Scholar 

23. Weis, P., Leroy, X.: Le langage Caml. InterEditions (1993), See also the CAML Web page: http://pauillac.inria.fr/caml/

24. Wenzel, M.: Isar - a generic intepretive approach to readable formal proof documents. In: Bertot et al. [2], pp. 167–183

    Google Scholar 

25. Whitehead, A.N., Russell, B.: Principia Mathematica, vol. 3. Cambridge University Press, Cambridge (1910)

    MATH  Google Scholar 

26. Zammit, V.: On the implementation of an extensible declarative proof language. In: Bertot et al. [2],pp. 185–202

    Google Scholar 

Download references