Nassima KACIMI-IZERROUKEN

What I'm interested in ?

• Compilers Verification and Validation
• Certified Code Generators
• Semantics
• Model Transformation
• Model Based Design Language for Critical Systems: Simulink/Stateflow, Scade, etc.
• Use of Formal Verification
• Proof Assistants : Coq, Isabelle
• Embedded Critical Real Time Systems
• Synchronous Languages

More details

PhD Research

There is an increasing awareness of the fact that the application of formal specification languages and their verification/validation reduce the risk of the design errors in the development of critical embedded systems. However, the verification process focused on the specification level can not ensure the safety of the system because of compiler bugs. My research focuses on the development and the formal verification using the proof assistant Coq of a code generator/compiler Simulink to C.

Publications

See also at [IRIT] -- [DBLP].

National Journals

• Expérimentations en COQ pour un générateur de code qualifiable.
  N. Izerrouken , M. Pantel and X. Thirioux O. Ssi Yan Kai
  Techniques et Sciences Informatiques 30(4), 409--440, 2011

International conferences articles

• Use of Formal Methods for Building Qualified Code Generator for Safer Automotive Systems
  N. Izerrouken , O. Ssi Yan Kai , M. Pantel and X. Thirioux
  ACM digital proceedings of CARS'10, colocated with EDCC (Position paper), 53--56
  April 27.-30. 2010, Valencia - Spain
• Towards Reliable Code Generation with an Open Tool: Evolutions of the Gene-Auto toolset
  A. Toom , N. Izerrouken , T. Naks , M. Pantel and O. Ssi Yan Kai
  Electronic proceedings of ERTS'10, (Regular paper)
  May 19.-21. 2010, Toulouse - France
• Machine-Checked Sequencer for Critical Embedded Code Generator
  N. Izerrouken , M. Pantel and X. Thirioux
  Springer LNCS proceedings of ICFEM'09,(Regular paper) 521--540
  December 09.-12. 2009, Rio De Janiero - Brazil (A.R:23%)
• Integrated Formal Approach for Qualified Critical Embedded Code Generator
  N. Izerrouken , M. Pantel, X. Thirioux, and O. Ssi Yan Kai
  Springer LNCS proceedings of FMICS'09, (Short paper+Poster), 199--201
  November 02.-03. 2009, Eindhoven - The Netherlands
• Certifying an Automated Code Generator Using Formal Tools: Preliminary Experiments in the GeneAuto Project
  N. Izerrouken , X. Thirioux, M. Pantel, and M. Strecker
  Electronic proceedings of ERTS'08, (Regular paper),
  January 29.-31.2008, February 1.2008, Toulouse - France

Technical reports

• D2.36: GeneAuto block sequencer tool requirements
  N. Izerrouken , M. Pantel and O. SSi Yan Kai
  Technical report of GeneAuto, August 2008
• D2.51: GeneAuto block sequencer tool design
  N. Izerrouken and M. Pantel
  Technical report of GeneAuto, September 2008
• GeneAuto Coq Development Guidelines
  N. Izerrouken and M. Pantel
  Technical report of GeneAuto European project. Presented to CEAT certification commitee, November 2008

Teaching

• Algorithmic, Programming and Object technologies JAVA (TP)
• Semantics and Compilation (TD and TP)
• Code Generation (TD and TP)
• Coq Proof Assistant (TP)

Some links

• citeseer - a scientific literature digital library and search engine focused on computer science
• conference-service - offers a directory of upcoming scientific and technical meetings
• eventseer - helps to keep track of academic events
• Publication Guidelines

Where and how to contact me ?

You can reach me at the "Bâtiment F" of IRIT-ENSEEIHT laboratory. I am working at the third floor, office F306.

I am also available by:

• phone: +33 (0)5 34 32 - 22 54
• fax: +33 (0)5 34 32 83 06
• e-mail : nassima.izerrouken@(NO_SPAM)enseeiht.fr

• and by snail mail:
  Institut de Recherche en Informatique de Toulouse
  Site N7 de l'IRIT-UMR CNRS 5505
  2, rue Charles Camichel
  BP 7122
  31071 Toulouse Cedex 7 France