[mihaela2014.jpg] Mihaela Sighireanu
ENS Paris-Saclay

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

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.
Last modified: Fri Sep 18 2020