Mihaela SIGHIREANU
Professor, ENS Paris-Saclay
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).
Please follow online SAS 2020!
SL-COMP'19 was hosted by
TOOLymics 2019 at
TACAS 2019
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)
Publications
On DBLP, Google Scholar, HAL, and 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
Teaching
My teaching experience is presented here. Now (fall 2020), I'm 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.
Proposals for graduate or undergraduate student internship
I'm also the director of studies for
Master 2 Research in Informatics at
Informatics Department of ENS Paris-Saclay.
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.