[mihaela2014.jpg] Mihaela Sighireanu
Associate Professor (Maître de conférences HDR)
University Paris Diderot

Office: SG 4021
Phone: +(33) 1 57 27 94 01
E-mail: firstname.lastname@irif.fr
Fax: +(33) 1 57 27 93 36
Mail: University Paris Diderot, 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:

  • Colis: Correctness of Linux Scripts (ANR-15-CE25-0001)
  • Vecolib: VErifying Automatically the Correct Use and Implementation of COntainer LIBraries (ANR ANR-14-CE28-0018-03)
  • Veridyc: Verification of C programs (ANR-09-SEGI-016)
  • AMAES: Formal Methods for Robotics (ANR)

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 Systems" specialization (engineering level) at EIDD

See also past courses, internships, educational services.

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: Wed Feb 12 2020