The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML

DOI10.1016/J.JLAP.2003.07.006MaRDI QIDQ1881670zbMATH OpenOpenAlexFDO

Authors Claude Marché, Christine Paulin-Mohring, Xavier Urbain

Publication date 14 October 2004

Published in The Journal of Logic and Algebraic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jlap.2003.07.006

zbMATH Keywords

ModelingFormal proofJAVAJML specifications

Mathematics Subject Classification ID

Theory of programming languages (68N15) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1848374
• JCML: A specification language for the runtime verification of Java card programs
• Specification and runtime verification of Java card programs

Cites work

• scientific article; zbMATH DE number 1612488 (Why is no real title available?)
• scientific article; zbMATH DE number 1617288 (Why is no real title available?)
• scientific article; zbMATH DE number 1701766 (Why is no real title available?)
• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 1848384 (Why is no real title available?)
• An Asymptotically Optimal Algorithm for the Dutch National Flag Problem
• How the design of JML accommodates both runtime assertion checking and formal verification
• Proving pointer programs in higher-order logic.
• The B-Book
• Verification of non-functional programs using interpretations in type theory
• Weakest pre-condition reasoning for Java programs with JML annotations

Cited in

(21)

• scientific article; zbMATH DE number 7566072 (Why is no real title available?)
• Secure information flow by self-composition
• Deductive verification of floating-point Java programs in KeY
• A program logic for resources
• scientific article; zbMATH DE number 7471663 (Why is no real title available?)
• Are the logical foundations of verifying compiler prototypes matching user expectations?
• Verification conditions for source-level imperative programs
• A dynamic logic for deductive verification of multi-threaded programs
• JCML: A specification language for the runtime verification of Java card programs
• Specification and runtime verification of Java card programs
• Could We Have Chosen a Better Loop Invariant or Method Contract?
• Weakest pre-condition reasoning for Java programs with JML annotations
• Cibai: An Abstract Interpretation-Based Static Analyzer for Modular Analysis and Verification of Java Classes
• Formalizing Single-Assignment Program Verification: An Adaptation-Complete Approach
• Verification of Java Programs with Generics
• An Introduction to Certificate Translation
• Reasoning about resources in the embedded systems language Hume
• Reasoning about object-based calculi in (co)inductive type theory and the theory of contexts
• Specification and verification challenges for sequential object-oriented programs
• A proof outline logic for object-oriented programming
• Synthesis of ML programs in the system Coq

Describes a project that uses

Uses Software

• LOOP
• JACK
• JML
• KRAKATOA
• Coq

This page was built for publication: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML

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