HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
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 Nancy - Grand Est, LORIA - FM - Department of Formal Methods
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 metadata

Contributor : Alain Giorgetti Connect in order to contact the contributor
Submitted on : Tuesday, October 23, 2007 - 11:35:42 AM
Last modification on : Friday, January 21, 2022 - 3:09:07 AM
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