Autres formats : [Format PDF] [Format Postscript]


Subject of a Post-Doc Position




Title

Timed Verification of Asynchronous Memories

Supervisors

Laurent Fribourg & Emmanuelle Encrenaz
Tél: +33 1 47 40 75 36 & + 33 1 44 27 20 38
Web: http://www.lsv.ens-cachan.fr/~fribourg & Web: http://www-asim.lip6.fr/~ema
Email: fribourg@lsv.ens-cachan.fr & emmanuelle.encrenaz@lip6.fr
Laboratoire Spécification et Vérification
École Normale Supérieure de Cachan
61, avenue du Président Wilson
94235 Cachan CEDEX

Description

The VALMEM project focuses on the functional and timed verification of embedded memory circuits. In this project, academic partners (LSV, LIP6) and industrial company (STMicroelectronics) share their complementary knowledges to tackle this verification problem using a specialized formal approach dedicated to “custom” circuit memories.

A semi-automatic method was presented in [CEFX09], and it allowed to verify an abstraction of the SPSMALL memory designed by STMicroelectronics. An “inverse method” was presented in [ACEF09], allowing to fully automatically optimize some timing bounds of this memory. This method, based on parametric timed automata, is limited by the size and the number of the components (gates) of the model.

The task of the post-doc researcher will be to face the scalability challenge by extending the inverse method. A direction of research will be to integrate compositionality into the method.

Remarks

The post-doc position is supported by the Agence Nationale de la Recherche, grant ANR-06-ARFU-005 (VALMEM project). Remuneration: about 20.000 EUR/year netto.

This position is for 12 months and should start between September 1st, 2009 and December 31st, 2009. Possible cheap accomodation inside the campus of ENS Cachan.

References

[ACEF09]
Étienne André, Thomas Chatain, Emmanuelle Encrenaz, and Laurent Fribourg. An inverse method for parametric timed automata. International Journal of Foundations of Computer Science, 2009. To appear.

[CEFX09]
R. Chevallier, E. Encrenaz, L. Fribourg, and W. Xu. Timed verification of the generic architecture of a memory circuit using parametric timed automata. Formal Methods in System Design, 34(1):59–81, February 2009.
Laboratoire Spécification et Vérification
This document was translated from LATEX by HEVEA.