Mihaela Sighireanu's Research Activities

Software Verification Timed Systems Model Checking Fault Tolerance Specification Languages

My research domain is about the application of formal methods to the development of complex systems, whatever their nature (hardware, software, or telecom). More precisely, my interests are in:

Modelling, specification, and formal analysis of computer systems.
Modelling of infinite state systems using extended automata (with counters, stacks, clocks).
Algorithms for verification of models with finite or infinite size (model-checking).
Software verification.
Semantics of programming languages.
Process algebra (CCS, CSP, LOTOS, E-LOTOS).

Other pages describing my research activities:

my resume,
a list of publications,
research projects I'm participating: Colis
past research projects I've been member: Vecolib, Bincoa, Veridyc Averiss (2006-2009), AMAES (2006-2009), Persee (2003-2006), ACI Jeunes Chercheurs (2002-2005), Advance (2001-2004), Tolere (1999), Verdon (1998).
activity report of LIAFA (in french),
my old home page at VASY team of INRIA.

Software Verification

Solver for Separation LOgic: SPEN and SL-COMP
Verification of programs with dynamic data structures: Cinv library, Celia tool
Verification of concurrent boolean programs with recursive procedure calls and rendez-vous communication: Spade tool
Verification of concurrent boolean programs with restricted communication: Press tool.

Model Checking: Finite and Infinite Systems

Verification of colored Petri nets (or rewriting systems with data). Application to verification of mutual exclusion protocols: CMRS tool.
Symbolic analysis of extended automata using TReX tool. TReX does symbolic reachability on products of automata extended with counters and clocks, and communicating by lossy FIFO-channels.
Contributor member to the CADP toolbox.
Applying model checking to verify protocols:
- IEEE 1394 (FireWire) Link layer protocol.
- Invoicing protocol.
Regular alternation-free mu-calculus used for robotics systems (in French) specified using ORCCAD.

Timed Systems

Using TGA and Uppaal for deriving temporal plans.
STNU strategies for TGA.

Fault Tolerance for Real-Time Embedded Systems

This work has been done during my Post-doctoral period in the TOLERE project.

DC2SDX: a translator from DC specifications to SynDEx specifications.
Heuristics for generation of fault-tolerant, automatically distributed code for embedded systems using AAA methodology and SynDEx.

Specification Languages for Parallel Systems: Semantics and Compilation

During my thesis, I developed a new language, called LOTOS NT, for the description of communication protocols. This language is an improvement of the LOTOS language, a process algebra based language. I also developed a compiler for LOTOS NT, called TRAIAN, which aims to translate LOTOS NT to an automata model in order to model check the description.

E-LOTOS: a new value-based asynchronous specification language for concurrent systems.
Contributor member of RSI (Romanian Institute for Standardization) at Enhancement to LOTOS Working Group of ISO.
TRAIAN: an E-LOTOS compiler designed using SYNTAX/FNC2
An Emacs mode for LOTOS specifications is available here.
Compilation of abstract data types (in french).

Last modified: Tue Feb 11 2020 Back to Mihaela's Home Page