Journal of Logic and Algebraic Programming, Volume 58

Volume 58, Numbers 1-2, January - March 2004

• Marieke Huisman, Thomas P. Jensen:
  Guest editors' introduction: Special issue on Formal Methods for Smart Cards. 1-2
  Electronic Edition (link) BibTeX
• Igor Siveroni:
  Operational semantics of the Java Card Virtual Machine. 3-25
  Electronic Edition (link) BibTeX
• Gerwin Klein, Martin Strecker:
  Verified bytecode verification and type-certifying compilation. 27-60
  Electronic Edition (link) BibTeX
• Bart Jacobs:
  Weakest pre-condition reasoning for Java programs with JML annotations. 61-88
  Electronic Edition (link) BibTeX
• Claude Marché, Christine Paulin-Mohring, Xavier Urbain:
  The KRAKATOA tool for certificationof JAVA/JAVACARD programs annotated in JML. 89-106
  Electronic Edition (link) BibTeX
• Bart Jacobs, Martijn Oostdijk, Martijn Warnier:
  Source code verification of a secure payment applet. 107-120
  Electronic Edition (link) BibTeX