Mihaela Sighireanu

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

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: Université de Paris, 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: 2017-2019: Colis: Correctness of Linux Scripts (ANR-15-CE25-0001) 2014-2018: Vecolib: VErifying Automatically the Correct Use and Implementation of COntainer LIBraries (ANR ANR-14-CE28-0018-03) 2009-2013: Veridyc: Verification of C programs (ANR-09-SEGI-016) 2005-2009: AMAES: Formal Methods for Robotics (ANR) Proposals for graduate or undergraduate student internship
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 Software Systems" specialization (engineering level) at EIDD See also past courses.
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.