Mihaela Sighireanu

	Mihaela Sighireanu Associate Professor (Maître de conférences HDR) IRIF University Paris Diderot

Contact	Office: SG 4021 Phone: +(33) 1 57 27 94 01 E-mail: firstname.lastname@irif.fr Fax: +(33) 1 57 27 93 36 Mail: University Paris Diderot, IRIF, case 7014, Sophie Germain Building 8 place Aurelie Nemours / F-75013 Paris France Access: directions
Curriculum	Biographical sketch Academic CV My HDR defense
Publications	DBLP, Google Scholar, HAL, My list B. Becker, N. Jeannerod, C. Marché, Y. Régis-Giannas, M. Sighireanu, and R. Treinen: Analysing installation scenarios of Debian packages at TACAS 2020
NEWS	Please submit to SAS 2020 in Chicago! Please submit to PAAR 2020 in Paris! In PC of ADSL 2020 SL-COMP'19 was hosted by TOOLymics 2019 at TACAS 2019
Research	My research focuses on models, algorithms, and tools for the verification and analysis of reliable systems, in particular: software analysis and verification (see also tool CELIA, projects Vecolib and Colis), decision procedures for program logics (see also solver Spen and SL-COMP), timed and parameterized systems (see also TReX), model-checking (see also CADP), fault tolerance, specification languages (see also TRAIAN). Present and past projects: Colis: Correctness of Linux Scripts (ANR-15-CE25-0001) Vecolib: VErifying Automatically the Correct Use and Implementation of COntainer LIBraries (ANR ANR-14-CE28-0018-03) Veridyc: Verification of C programs (ANR-09-SEGI-016) AMAES: Formal Methods for Robotics (ANR)
Teaching	Software Security (in French, licence 3) at UFR d'Informatique, Network programming (in French, licence 3) at UFR d'Informatique, Operating Systems and Networks at EIDD, Advanced Programming in Java (in French, Master 1) at EIDD, Programming in C (in French, Licence 3), at EIDD, Formal verification methods (in French, Master 2) at UFR d'Informatique, Director of studies for "Embedded Systems" specialization (engineering level) at EIDD See also past courses, internships, educational services.
Software	SPEN: solver for Separation Logic, Celia: verification and analysis of C programs with lists, Spade: analysis of Synchronized PAD, Press: bounded reachability in PRS, TReX: verification of parameterized extended automata, TRAIAN: compiler for LNT data structures, CADP: toolbox for model-checking, DC2SDX: translator of synchronous languages common format.