This paper presents an extension of the standard bitvector library of the theorem prover PVS with multiplication, division and remainder operations, together with associated results. This extension is needed to give correct semantics to Java’s integral types in program verification. Special emphasis is put on Java’s widening and narrowing functions in relation to the newly defined operations on bitvectors.


Smart Card Theorem Prove Object Constraint Language Java Program Integral Type 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Ahrendt, W., Baar, T., Beckert, B., Giese, M., Hähnle, R., Menzel, W., Mostowski, W., Schmitt, P.H.: The KeY system: Integrating object-oriented design and formal methods. In: Kutsche, R.-D., Weber, H. (eds.) FASE 2002. LNCS, vol. 2306, pp. 327–330. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  2. 2.
    Beckert, B., Schlager, S.: Integer arithmetic in the specification and verification of Java programs. In: Workshop on Tools for System Design and Verification, FM-TOOLS (2002),
  3. 3.
    van den Berg, J., Jacobs, B.: The LOOP compiler for Java and JML. In: Margaria, T., Yi, W. (eds.) TACAS 2001. LNCS, vol. 2031, pp. 299–312. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. 4.
    Carreño, V.A., Miner, P.S.: Specification of the IEEE-854 floating-point standard in HOL and PVS. In: Schubert, E.T., Windley, P.J., Alves-Foss, J. (eds.) Higher Order Logic Theorem Proving and Its Applications. Category B Proceedings (1995)Google Scholar
  5. 5.
    Chalin, P.: Improving jml: For a safer and more effective language. In: Formal Methods Europe 2003 (2003) (to appear)Google Scholar
  6. 6.
    Chen, Z.: Java Card Technology for Smart Cards. The Java Series. Addison-Wesley, Reading (2000)Google Scholar
  7. 7.
    Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., Stata, R.: Extended static checking for Java. In: Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). SIGPLAN Notices, vol. 37(5), pp. 234–245. ACM, New York (2002)CrossRefGoogle Scholar
  8. 8.
    Gosling, J., Joy, B., Steele, G., Bracha, G.: The Java Language Specification, 2nd edn. The Java Series. Addison-Wesley, Reading (2000)zbMATHGoogle Scholar
  9. 9.
    Harrison, J.: A machine-checked theory of floating point arithmetic. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin, C., Théry, L. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 113–130. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  10. 10.
    Harrison, J.: Formal verification of IA-64 division algorithms. In: Aagaard, M.D., Harrison, J. (eds.) TPHOLs 2000. LNCS, vol. 1869, pp. 234–251. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  11. 11.
    Jacobs, B., Oostdijk, M., Warnier, M.: Formal verification of a secure payment applet. Journ. of Logic and Algebraic Programming (to appear)Google Scholar
  12. 12.
    Leavens, G.T., Baker, A.L., Ruby, C.: JML: A notation for detailed design. In: Kilov, H., Rumpe, B. (eds.) Behavioral Specifications of Business and Systems, pp. 175–188. Kluwer, Dordrecht (1999)CrossRefGoogle Scholar
  13. 13.
    Leavens, G.T., Poll, E., Clifton, C., Cheon, Y., Ruby, C.: JML reference manual, draft (2003),
  14. 14.
    Marché, C., Paulin, C., Urbain, X.: The Krakatoa tool for certification java/javacard programs annotated in jml. Journ. of Logic and Algebraic Programming (to appear)Google Scholar
  15. 15.
    Owre, S., Rushby, J.M., Shankar, N., von Henke, F.: Formal verification for fault-tolerant architectures: Prolegomena to the design of PVS. IEEE Trans. on Softw. Eng. 21(2), 107–125 (1995)CrossRefGoogle Scholar
  16. 16.
    Rauch, N., Wolff, B.: Formalizing Java’s two’s-complement integral type in Isabelle/HOL. In: Arts, T., Fokkink, W. (eds.) Formal Methods for Industrial Critical Systems (FMICS 2003). Elect. Notes in Theor. Comp. Sci, vol. 80. Elsevier, Amsterdam (2003), Google Scholar
  17. 17.
    Stallings, W.: Computer Organization and Architecture, 4th edn. Prentice Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar
  18. 18.
    Théry, L.: A library for floating-point numbers in Coq (2002),
  19. 19.
    Winkler, J.F.H.: A safe variant of the unsafe integer arithmetic of Java TM. Software – Practice and Experience 33, 669–701 (2002)CrossRefzbMATHGoogle Scholar

Copyright information

© IFIP International Federation for Information Processing 2003

Authors and Affiliations

  • Bart Jacobs
    • 1
  1. 1.Dep. Comp. Sci.Univ. NijmegenNijmegenThe Netherlands

Personalised recommendations