A formal executable semantics of the JavaCard platform

DOI10.1007/3-540-45309-1_20MaRDI QIDQ2763680zbMATH OpenFDO

Authors Gilles Barthe, Guillaume Dufay, Line Jakubiec, Bernard Paul Serpette, Simão Melo de Sousa

Publication date 21 January 2002

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/2028/20280302

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Specification and verification (program logics, model checking, etc.) (68Q60) Computing methodologies and applications (68U99)

Recommendations

• Algebraic Methodology and Software Technology
• scientific article; zbMATH DE number 2086505
• scientific article; zbMATH DE number 2043539
• Fundamental Approaches to Software Engineering
• Correctness of Java Card method lookup via logical relations

Cited in

(20)

• A B model for ensuring soundness of a large subset of the Java card virtual machine
• Verified bytecode verifiers.
• Operational semantics of the Java Card Virtual Machine
• Verified bytecode verification and type-certifying compilation
• Extracting a data flow analyser in constructive logic
• Correctness of Java Card method lookup via logical relations
• Specification of a smart card operating system
• Formal methods in context: security and Java card
• Formal specification and verification of JavaCard's application identifier class
• Animating the formalised semantics of a Java-like language
• Certified Static Analysis by Abstract Interpretation
• CoqJVM: An Executable Specification of the Java Virtual Machine Using Dependent Types
• scientific article; zbMATH DE number 2043539 (Why is no real title available?)
• scientific article; zbMATH DE number 1927413 (Why is no real title available?)
• scientific article; zbMATH DE number 2086505 (Why is no real title available?)
• scientific article; zbMATH DE number 1848380 (Why is no real title available?)
• scientific article; zbMATH DE number 1848384 (Why is no real title available?)
• Algebraic Methodology and Software Technology
• Fundamental Approaches to Software Engineering
• Tool-assisted specification and verification of typed low-level languages

Describes a project that uses

Uses Software

• Coq
• DrScheme

This page was built for publication: A formal executable semantics of the JavaCard platform

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