Skip to Main content Skip to Navigation
Conference papers

Un programme annoté en vaut deux

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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : Formal verification methods could be of much help to increase software safety. But how to transfer these methods in the real world of critical software development? This paper proposes a tooled solution for source code verification, by automated reduction of safety properties into formal assertions. This approach is applied to JML annotated Java programs. It is illustrated by the automated generation of assertions for a class from the Java Card API. Two complementary formalisms are proposed for expressing properties. Their reduction in JML annotations is implanted in the JAG tool, described with details. The output language (JML) being standard, this tool interfaces easily with many standard tools for verification of JML/Java code by proof ou model-checking.
Complete list of metadatas
Contributor : Alain Giorgetti <>
Submitted on : Tuesday, October 23, 2007 - 11:35:42 AM
Last modification on : Tuesday, October 27, 2020 - 2:34:29 PM
Long-term archiving on: : Sunday, April 11, 2010 - 11:37:08 PM


Files produced by the author(s)


  • HAL Id : inria-00181135, version 1


Alain Giorgetti, Julien Groslambert. Un programme annoté en vaut deux. Journée Francophone des Langages Applicatifs - JFLA07, Jan 2007, Aix-les-Bains, France. ⟨inria-00181135⟩



Record views


Files downloads