JACK — A Tool for Validation of Security and Behaviour of Java Applications. 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.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Fähndrich, Manuel; Logozzo, Francesco: Static contract checking with abstract interpretation (2011)
- du Bousquet, Lydie; Ledru, Yves; Maury, Olivier; Oriat, Catherine; Lanet, Jean-Louis: Reusing a JML specification dedicated to verification for testing, and vice-versa: Case studies (2010) ioport
- James, Perry R.; Chalin, Patrice: Faster and more complete extended static checking for the Java modeling language (2010)
- Barthe, Gilles; Burdy, Lilian; Charles, Julien; Grégoire, Benjamin; Huisman, Marieke; Lanet, Jean-Louis; Pavlova, Mariela; Requet, Antoine: JACK -- a tool for validation of security and behaviour of Java applications (2007) ioport
- Logozzo, Francesco: Cibai: An abstract interpretation-based static analyzer for modular analysis and verification of Java classes (2007)
- Nguyen, Quang-Huy; Chetali, Boutheina: Certifying native Java card API by formal refinement (2006) ioport
- Marché, C.; Paulin-Mohring, C.; Urbain, X.: The KRAKATOA tool for certification of JAVA/JAVACARD programs annotated in JML (2004)