Skip to Main content Skip to Navigation
Reports

JAG : Génération d'annotations JML pour vérifier des propriétés temporelles

Alain Giorgetti 1 Julien Groslambert 2 
1 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : This paper presents a tool for verifying security properties on Java code enriched with JML annotations. These temporal properties are expressed in an extension of JML. They are translated by the tool into standard JML annotations and are automatically integrated in the Java class under verification. This paper is an extended version of a paper presented at AFADL'06 tool session.
Document type :
Reports
Complete list of metadata

https://hal.inria.fr/inria-00114317
Contributor : Alain Giorgetti Connect in order to contact the contributor
Submitted on : Thursday, November 16, 2006 - 11:59:34 AM
Last modification on : Friday, January 21, 2022 - 3:08:59 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 7:10:33 PM

Identifiers

  • HAL Id : inria-00114317, version 1

Citation

Alain Giorgetti, Julien Groslambert. JAG : Génération d'annotations JML pour vérifier des propriétés temporelles. [Research Report] 2006. ⟨inria-00114317⟩

Share

Metrics

Record views

130

Files downloads

102