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

DOI10.1016/j.jlap.2003.07.006zbMath1073.68678OpenAlexW1996228525MaRDI QIDQ1881670

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

ModelingJAVAFormal proofJML specifications

Mathematics Subject Classification ID

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

Related Items (21)

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

Uses Software

• Coq
• KRAKATOA
• JML
• JACK
• LOOP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• How the design of JML accommodates both runtime assertion checking and formal verification
• Weakest pre-condition reasoning for Java programs with JML annotations
• An Asymptotically Optimal Algorithm for the Dutch National Flag Problem
• The B-Book
• Verification of non-functional programs using interpretations in type theory
• Automated Deduction – CADE-19

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