Validation of the JavaCard platform with implicit induction techniques

DOI10.1007/3-540-44881-0_24MaRDI QIDQ4447243zbMATH OpenFDO

Authors Gilles Barthe, Sorin Stratulat

Publication date 16 February 2004

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/2706/27060337.htm

Mathematics Subject Classification ID

Theory of software (68N99) Grammars and rewriting systems (68Q42)

Recommendations

• A formal executable semantics of the JavaCard platform
• Tool-assisted specification and verification of typed low-level languages
• Fundamental Approaches to Software Engineering
• Java bytecode verification: Algorithms and formalizations
• On-card bytecode verification for Java card

Cited in

(9)

• Correctness of Java card method lookup via logical relations
• A B model for ensuring soundness of a large subset of the Java card virtual machine
• Correctness of Java Card method lookup via logical relations
• A formal executable semantics of the JavaCard platform
• Automated Certification of Implicit Induction Proofs
• Combining Rewriting with Noetherian Induction to Reason on Non-orientable Equalities
• scientific article; zbMATH DE number 2086505 (Why is no real title available?)
• Mechanically certifying formula-based Noetherian induction reasoning
• Tool-assisted specification and verification of typed low-level languages

Describes a project that uses

Uses Software

• SPIKE
• Coq
• Jakarta

This page was built for publication: Validation of the JavaCard platform with implicit induction techniques

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