JavaCard Program Verification

1. J. van den Berg and B. Jacobs. The LOOP compiler for Java and JML. In T. Margaria and W. Yi, editors, Tools and Algorithms for the Construction and Analysis of Software (TACAS), number 2031 in Lect. Notes Sci., pages 299–312. Springer, Berlin, 2001.

   Chapter  Google Scholar 

2. J. van den Berg, B. Jacobs, and E. Poll. Formal specification and verification of JavaCard’s Application Identifier Class. In I. Attali and Th. Jensen, editors, Proceedings of the Java Card 2000 Workshop, Lect. Notes Sci. Springer, Berlin, 2001.

   Google Scholar 

3. Z. Chen. Java Card Technology for Smart Cards. The Java Series. Addison-Wesley, 2000.

   Google Scholar 

4. B. Jacobs and E. Poll. A logic for the Java Modeling Language JML. In H. Hussmann, editor, Fundamental Approaches to Software Engineering (FASE), number 2029 in Lect. Notes Sci., pages 284–299. Springer, Berlin, 2001.

   Chapter  Google Scholar 

5. G.T. Leavens, A.L. Baker, and C. Ruby. JML: A notation for detailed design. In H. Kilov and B. Rumpe, editors, Behavioral Specifications of Business and Systems, pages 175–188. Kluwer, 1999.

   Google Scholar 

6. E. Poll, J. van den Berg, and B. Jacobs. Formal specification of the JavaCard API in JML: The APDU class. Networks Mag., 2001. To appear.

   Google Scholar 

Download references