The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
type: Item
instance of: scholarly article
title: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML
zbMATH Open document ID: 1073.68678
published in: The Journal of Logic and Algebraic Programming
publication date: 2004-10-14T00:00:00Z
Mathematics Subject Classification ID: 68Q60
Mathematics Subject Classification ID: 68N15
zbMATH DE Number: 2107871
zbMATH Keywords: JAVA
zbMATH Keywords: JML specifications
zbMATH Keywords: Modeling
zbMATH Keywords: Formal proof
author: Claude Marché
author: Christine Paulin-Mohring
author: Xavier Urbain
describes a project that uses: JML
describes a project that uses: Coq
describes a project that uses: JACK
describes a project that uses: KRAKATOA
describes a project that uses: LOOP
MaRDI profile type: Publication
full work available at URL: j.jlap.2003.07.006
OpenAlex ID: W1996228525
cites work: Q4785558
cites work: Q2722012
cites work: Q2769594
cites work: The B-Book
cites work: Weakest pre-condition reasoning for Java programs with JML annotations
cites work: Verification of non-functional programs using interpretations in type theory
cites work: Q4144755
cites work: An Asymptotically Optimal Algorithm for the Dutch National Flag Problem
cites work: How the design of JML accommodates both runtime assertion checking and formal verification
cites work: Q2721096
cites work: Automated Deduction – CADE-19
DOI: 10.1016/J.JLAP.2003.07.006
Recommended article: Q4785541
Recommended article: JCML: A specification language for the runtime verification of Java card programs
Recommended article: Specification and Runtime Verification of Java Card Programs
description: scientific article; zbMATH DE number 2107871