A program logic for handling Java Card's transaction mechanism

DOI10.1007/3-540-36578-8_18MaRDI QIDQ4417836zbMATH OpenFDO

Authors Bernhard Beckert, Wojciech Mostowski

Publication date 30 July 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/2621/26210246.htm

Mathematics Subject Classification ID

Logic in computer science (03B70) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Specification and runtime verification of Java card programs
• A programming and a modelling perspective on the evaluation of Java card implementations
• A flexible invocation framework for Java Card
• A dynamic logic for the formal verification of Java card programs
• Towards a full formal specification of the JavaCard API
• Implementation of Java card virtual machine
• A simple(r) interface distribution mechanism for Java card
• On-card bytecode verification for Java card

Cited in

(4)

• A program logic for resources
• CardKt: Automated multi-modal deduction on Java cards for multi-application security
• A dynamic logic with traces and coinduction
• Certification Using the Mobius Base Logic

This page was built for publication: A program logic for handling Java Card's transaction mechanism

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