next up previous
Next: A2- Équipes ou laboratoires Up: Description-SI Previous: A1 - Coordinateur du

A2- Équipes ou laboratoires partenaires du Projet 6:

Identification de l'équipe ou du laboratoire
 Équipe ou Laboratoire  VERIMAG UMR 5104
 Adresse  Centre Equation
   2, Ave Vignate
   38610 Gières

Organisme de rattachement financier de l'équipe pour le présent projet
 CNRS

Responsable du projet au sein de l'équipe ou du laboratoire
 M. ou Mme. Prénom Nom  M. Sergio Yovine
 Fonction  CR1 CNRS
 Téléphone  04 76 63 48 43
 Fax  04 76 63 48 50
 Mél  Sergio.Yovine@imag.fr

Autres membres de l'équipe participant au projet
Nom Prénom Poste statutaire % du temps de
      recherche
      consacré au projet
 Iosif  Radu  CR2 CNRS  80%
 Bozga  Marius  IR2 CNRS  50%
 Lakhnech  Yassine  Professeur  20%
 Nakhli  Chaker  Doctorand  30%
 Amrani  Moussa  Doctorand  70%

Références :
Pour chaque (enseignant-)chercheur participant, liste de 3 à 5 publications, logiciels ou brevets les plus significatifs, en relation avec la thématique du projet.
 
Sergio Yovine :
 
Ch. Kloukinas, S. Yovine. Synthesis of Safe, QoS Extendible, Application Specific Schedulers for Heterogeneous Real-Time Systems. 15th Euromicro Conference on Real-Time Systems, 2003 (à paraître).
 
J. Sifakis, S. Tripakis, S. Yovine. Building models of real-time systems from application software. Proceedings of the IEEE, Special issue on modeling and design of embedded, 91(1):100-111, January 2003.
 
V. Colin de Verdiere, S. Cros, C. Fabre, R. Guider, S. Yovine. Speedup Prediction for Selective Compilation of Embedded Java Programs. Workshop on Embedded Software, EMSOFT'02. LNCS 2491, Springer-Verlag.
 
V. Bertin, E. Closse, M. Poize, J. Pulou, J. Sifakis, P. Venier, D. Weil, S. Yovine. Taxys = Esterel + Kronos. A tool for verifying real-time properties of embedded systems. Conference on Decision and Control, CDC'01. IEEE Control Systems Society, 2001.
 
S. Yovine. Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer, Vol. 1, Issue 1/2, pages 123-133, October 1997. Springer-Verlag.
 
 
Radu Iosif :
 
R. Iosif. Symmetry Reduction Criteria for Software Model Checking. Proc. 9th SPIN Workshop on Software Model Checking. Lecture Notes in Computer Science, Volume 2318, Springer Verlag, April 2002.
 
R. Iosif. Exploiting Heap Symmetries in Explicit-State Model Checking of Software. Proc 16th IEEE International Conference on Automated Software Engineering, pp. 254 - 261, November 2001.
 
R. Iosif, R. Sisto. Temporal Logic Properties of Java Objects. Proc 13th International Conference on Software Engineering & Knowledge Engineering, March 2001.
 
R. Iosif, R. Sisto. Using Garbage Collection in Model Checking. Proc. 7th SPIN Workshop, Lecture Notes in Computer Science, Volume 1885, pp. 20 - 33, September 2000.
 
R. Iosif. Formal Verification Applied to Java Concurrent Software. Proc. 22nd International Conference on Software Engineering (Doctoral Workshop), pp. 707 - 709, June 2000.
 
 
Marius Bozga :
 
M. Bozga, S. Graf, L. Mounier. IF-2.0: A Validation Environment for Component-Based Real-Time Systems. Proceedings of CAV'02 (Copenhagen, Denmark) LNCS 2404, Springer July 2002.
 
M. Bozga, S. Graf, L. Mounier. Automated validation of distributed software using the IF environment. Workshop on Software Model-checking. Electronic Notes in Theoretical Computer Science, 55. Elsevier Science Publishers, July 2001.
 
M. Bozga, S. Graf, L. Mounier, I. Ober, J.L. Roux, D. Vincent. Timed Extensions for SDL In Proceedings of SDL FORUM'01 (Copenhagen, Denmark) LNCS 2078, Springer, June 2001.
 
M. Bozga, D. Lesens, L. Mounier. Model-Checking Ariane-5 Flight Program In Proceedings of FMICS'01 (Paris, France), INRIA 2001.
 
M. Bozga, J.C. Fernandez, L. Ghirvu, S. Graf, J.P. Krimm, L. Mounier. IF: A Validation Environment for Timed Asynchronous Systems. CAV'00, LNCS, Springer-Verlag, July 2000.
 
 
Yassine Lakhnech :
 
D. Dams, Y. Lakhnech, M. Steffen. Iterating Transducers. Journal of Logic and Algebraic Programming. Volumes 52-53, Pages 109-127, July-August 2002.
 
K. Baukus, Y. Lakhnech, K. Stahl. Parameterized Verification of a Cache Coherence Protocol: Safety and Liveness. Verification, Model Checking, and Abstract Interpretation, Third International Workshop, VMCAI, 2002: 317-330. Lecture Notes in Computer Science 2294, Springer, 2002.
 
Y. Lakhnech, S. Bensalem, S. Berezin, S. Owre. Incremental Verification by Abstraction. Tools and Algorithms for the Construction and Analysis of Systems, LNCS 2031, Springer-Verlag, 2001.
 
W.P. de Roever, F. de Boer, U. Hanneman, Y. Lakhnech, M. Poel, J. Zwiers. Concurrency Verification: Introduction to Compositonal and Noncompositional Methods. Cambridge University Press, 2001.
 
P. Abdulla, A. Annichini, S. Bensalem, A. Bouajjani, P. Habermehl, Y. Lakhnech. Verification of Infinite-State Systems by Combining Abstraction and Reachability Analysis. Computer Aided Verification'99, LNCS 1633, Springer-Verlag, 1999.
 

Action Concertée Incitative

SÉCURITÉ INFORMATIQUE

Descriptif complet du projet


next up previous
Next: A2- Équipes ou laboratoires Up: Description-SI Previous: A1 - Coordinateur du
Radu Iosif 2003-09-20