Specification and runtime verification of Java card programs

DOI10.1016/J.ENTCS.2009.05.045MaRDI QIDQ5179352zbMATH OpenOpenAlexFDO

Authors Umberto Souza da Costa, Anamaria Martins Moreira, Martin A. Musicante, Plácido A. Souza Neto

Publication date 19 March 2015

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2009.05.045

zbMATH Keywords

compilerJava cardJCMLJMLruntime verification

Mathematics Subject Classification ID

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Theory of compilers and interpreters (68N20) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• JCML: A specification language for the runtime verification of Java card programs
• scientific article; zbMATH DE number 1857507
• scientific article; zbMATH DE number 1848374
• scientific article; zbMATH DE number 1706337
• Fundamental Approaches to Software Engineering

Cites work

• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 605917 (Why is no real title available?)
• KeY: A Formal Method for Object-Oriented Systems
• The B-Book
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML

Cited in

(9)

• Correctness of Java card method lookup via logical relations
• The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
• Laws of mission-based programming
• Safety-critical Java programs from \textsf{Circus} models
• scientific article; zbMATH DE number 1706331 (Why is no real title available?)
• JCML: A specification language for the runtime verification of Java card programs
• scientific article; zbMATH DE number 1956492 (Why is no real title available?)
• scientific article; zbMATH DE number 2087509 (Why is no real title available?)
• scientific article; zbMATH DE number 1848374 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• KRAKATOA
• Eiffel
• Daikon
• JML
• JCML
• Z
• LOOP

This page was built for publication: Specification and runtime verification of Java card programs

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