|
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.
|
|