Documentation
Here you will find some documentation that gives a description of how to use and how works JACK.
User Documentation:
(Some drafts)
Tutorial (FM 05 - July 2005):
Developer Documentation:
Publications
L. Burdy, A. Requet, J.-L. Lanet.
Java Applet Correctness: A Developer-Oriented Approach.
ps
pdf
bib
G. Barthe and P. D'Argenio and T. Rezk.
Secure Information Flow by Self-Composition
ps
pdf
bib
M. Pavlova and G. Barthe and L. Burdy and M. Huisman and J.-L. Lanet.
Enforcing High-Level Security Properties For Applets
ps
pdf
bib
G. Barthe and M. Pavlova and G. Schneider.
Precise analysis of memory consumption using program logics
pdf
bib
L. Burdy and M. Pavlova.
Java Bytecode Specification and Verification
pdf
bib
J. Charles. Adding Native Specifications to JML
ps
bib
G. Barthe, L. Burdy, J. Charles
B. Grégoire, M. Huisman, J.-L. Lanet,
M. Pavlova and A. Requet.
JACK: a tool for validation of security and behaviour of Java applications
pdf
bib