Mihaela Sighireanu

	Mihaela Sighireanu Professor LSV ENS Paris-Saclay

Contact	Office: 2U26 Phone: +(33) 1 81 87 54 65 E-mail: firstname.lastname@lsv.fr Mail: LSV, ENS Paris-Saclay 4 avenue des Sciences F-91190 Gif-sur-Yvette 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	I'm now at LSV! Please consider my new address. Please follow online SAS 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	Programming (in French, licence 3) at Informatics Department of ENS Paris-Saclay, Logic for Artificial Intelligence (Master 1 MPRI) at Informatics Department of ENS Paris-Saclay, Working group on decision procedures for separation logic (Master 1 MPRI) at Informatics Department of ENS Paris-Saclay, Networks (Master 1 MPRI) at Informatics Department of ENS Paris-Saclay. Director of studies for Master 2 Research in Informatics at Informatics Department of ENS Paris-Saclay. 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.