Mihaela Sighireanu graduated as a Computer Science Engineer at the "Politehnica" University of Bucarest (Romania) in 1994. She carried out the engineering training (six months) in France, at Verimag laboratory, on the compilation of the abstract data types of LOTOS. Mihaela's engineering training was funded by the European Commission under the Tempus program. In July 1995, she obtained the Master of Science degree (Diplôme d'Etudes Approfondies) in Computer Science from IMAG. During her master, she worked on the optimization of the CAESAR.ADT compiler, which is part of the CADP toolbox. This compiler translates the data part of LOTOS specifications into libraries of C types and functions. Mihaela's Master of Science was funded by the Rhone-Alpes Region under the Tempra program.
From November 1995 to December 1998, Mihaela worked on the improvement of formal description technique LOTOS. This work ended up at the definition of a new formalism, called LOTOS NT, for the formal description of parallel and real time applications. This formalism, which combines concepts from functional and imperative programming languages and timed process algebras, is simpler and more expressive than the existing formal description techniques (in particular, the three standardized languages ESTELLE, LOTOS, and SDL) and allows more efficient compiling techniques. The work on LOTOS NT represented a contribution to the revision of the standard LOTOS undertaken at ISO. She also was the main designer and developer of the first and second versions of the TRAIANcompiler for LOTOS NT.
Besides this, Mihaela Sighireanu worked on the verification of several protocols, the most important being the IEEE 1394 (FireWire) protocol.
Mihaela obtained her Ph.D. Thesis in Computer Science in January 1999 with a thesis entitled "Contribution at the definition and the implementation of Extended LOTOS language". Her Ph.D. grant was funded by the European Pole and French Ministry of Education and Research.
In January 1999, Mihaela Sighireanu joined the BIP team of INRIA Rhône-Alpes and worked on fault tolerance of embedded systems within the TOLERE project. She applied her knowledge of model checking and compilation tools to provide new model checking capabilities inside the ORCCAD tool and to connect the DC language (common format of the synchronous languages Esterel, Lustre, and Signal) to the SynDEx tool.
In September 1999, she obtained a permanent academic position (Maître de Conférences) at the University of Paris 7. Now, she is working on formal methods and model checking at the LIAFA Laboratory. Mihaela's present activities are described on her personal page at LIAFA.