Towards a full formal specification of the JavaCard API

DOI10.1007/3-540-45418-7_14MaRDI QIDQ4785558zbMATH OpenFDO

Authors Hans Meijer, Erik Poll

Publication date 5 January 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2140/21400165

Mathematics Subject Classification ID

Data encryption (aspects in computer science) (68P25) Computing methodologies and applications (68U99)

Recommendations

• Formal specification and verification of JavaCard's application identifier class
• Algebraic Methodology and Software Technology
• A formal executable semantics of the JavaCard platform
• Formal methods for smart cards: an experience report
• JCML: A specification language for the runtime verification of Java card programs

Cited in

(10)

• Weakest pre-condition reasoning for Java programs with JML annotations
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Formal methods in context: security and Java card
• A simple(r) interface distribution mechanism for Java card
• Formal specification and verification of JavaCard's application identifier class
• JCML: A specification language for the runtime verification of Java card programs
• A program logic for handling Java Card's transaction mechanism
• An operational semantics of the Java Card firewall
• A flexible invocation framework for Java Card
• scientific article; zbMATH DE number 2090142 (Why is no real title available?)

Describes a project that uses

Uses Software

• JML
• LOOP

This page was built for publication: Towards a full formal specification of the JavaCard API

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4785558)