JACK - A Tool for Validation of Security and Behaviour of Java Applications

Gilles Barthe, Lilian Burdy, Julien Charles, Benjamin Grégoire, Marieke Huisman, Jean-Louis Lanet, Mariela Pavlova, Antoine Requet

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

We describe the main features of JACK (Java Applet Correctness Kit), a tool for the validation of Java applications, annotated with JML specifications. JACK has been especially designed to improve the quality of trusted personal device applications. JACK is fully integrated with the IDE Eclipse, and provides an easily accessible user interface. In particular, it allows to inspect the generated proof obligations in a Java syntax, and to trace them back to the source code that gave rise to them. Further, JACK provides support for annotation generation, and for interactive verification. The whole platform works both for source code and for bytecode, which makes it particularly suitable for a proof carrying code scenario.
Original languageEnglish
Title of host publicationFormal Methods for Components and Objects, 5th International Symposium, FMCO 2006, Amsterdam, The Netherlands, November 7-10, 2006, Revised Lectures
EditorsFrank S. de Boer, Marcello M. Bonsangue, Susanne Graf, Willem P. de Roever
PublisherSpringer Singapore
Pages152-174
Number of pages23
DOIs
Publication statusPublished - 2006
Externally publishedYes
Event5th International Symposium on Formal Methods for Components and Objects, FMCO 2006 - Amsterdam, Netherlands
Duration: 7 Nov 200610 Nov 2006
Conference number: 5

Publication series

NameLecture Notes in Computer Science
PublisherSpringer
Volume4709

Conference

Conference5th International Symposium on Formal Methods for Components and Objects, FMCO 2006
Abbreviated titleFMCO 2006
CountryNetherlands
CityAmsterdam
Period7/11/0610/11/06

Fingerprint Dive into the research topics of 'JACK - A Tool for Validation of Security and Behaviour of Java Applications'. Together they form a unique fingerprint.

Cite this