Mihaela Sighireanu
Professor, ENS Paris-Saclay
Director of studies Computer Science Departement
Mail: msighireanu@lmf.cnrs.fr
Phone: +33 (0)1 81 87 54 65
Office: 1S57, Bâtiment ENS - Nord
Laboratoire Méthodes Formelles (LMF)
Université Paris-Saclay, CNRS, ENS Paris-Saclay
4 avenue des Sciences • 91190 Gif-sur-Yvette, France
Some pointers on my 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 project Narco, solver Spen and SL-COMP), timed and parameterized systems (see also TReX), model-checking (see also CADP), fault tolerance, specification languages (see also TRAIAN).
- My publications
- My DBLP profile; my google scholar profile
- My curriculum vitae in English (March 2020)
Professional activities
- I was in the PC of CAV'24, TACAS'24, VMCAI'24, CAV'23, SAS'23, VMCAI'23, ATVA'22, SAS'22, ...
- I was in charge of organizing SL-COMP an international competition for Separation Logic solvers
- I have been the PC co-chair of the conference SAS'20
- I was director of studies for the Computer Science course of studies at EIDD (2018--2020)
- I previously teach at University Paris-Diderot and did my research at IRIF.
Students supervision
- I co-supervise two PhD students:
- Julien Simonnet: started in Nov. 2021, co-supervised by Matthieu Lemerre
- Quentin Petitjean: started in Sep. 2022, co-supervised by Nicolas Peltier
- Past PhD students co-supervised:
- Fang Bin
- Cezara Dragoi
Projects
Ongoing projects
- Narco Non-Aggregative Resource COmpositions
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)
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