Mihaela Sighireanu's Publications
Journals
Books
Conferences
Research Reports
ISO Reports
Thesis
Journals
-
Formal modelling of list based dynamic memory allocators.
Bin Fang, Mihaela Sighireanu, Geguang Pu, Wen Su, Jean-Raymond Abrial,
Mengfei Yang, and Lei Qiao
SCIENCE CHINA Information Sciences 61(12): 122103:1--122103:16 (2018).
-
Compositional Entailment Checking for a Fragment of Separation Logic.
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomas Vojnar.
Formal Methods in System Design 51(3): 575-607 (2017).
- Report on SL-COMP 2014
Mihaela Sighireanu and David R. Cok.
JSAT 9: 173-186 (2014).
- A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes.
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Yan Jurski, Mihaela Sighireanu.Logical Methods in Computer Science 5(2): (2009). [ArXiv]
- Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus.
R. Mateescu and M. Sighireanu, Science of Computer Programming 46(3):255-281, March 2003.
- Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS.
M. Sighireanu and R. Mateescu, Springer International Journal on Software Tools for Technology Transfer (STTT), 2(1):68-88, 1998.
Chapter's Book
- Introduction à E-LOTOS.
G. Leduc, A. Jeffrey, and M. Sighireanu, Chapitre 6 in Ingenierie
des protocoles et qualite de service, A. Cavalli editor,
Hermes, collection IC2, pages 213-253, 2001.
- ELOTOS: (Enhanced) Language Of Temporal Ordering Specification.
K.J. Turner and M. Sighireanu, Chapter 10 in Software
Specification Methods, M. Frappier and H. Habrias editors,
Springer-Verlag, pages 166-190, 2001.
(Also published by Hermes and Lavoisier in 2006.)
Conferences and workshops
-
Analysing installation scenarios of Debian packages
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Giannas, Mihaela Sighireanu and Ralf Treinen.
LNCS.
In Proceedings of TACAS 2020.
-
TOOLympics 2019: An Overview of Competitions in Formal Methods
Ezio Bartocci et al.
Proceedings of TACAS'19
LNCS 11429, DOI: 10.1007/978-3-030-17502-3_1.
-
SL-COMP: Competition of Solvers for Separation Logic.
Mihaela Sighireanu and al.
Proceedings of TACAS'19
LNCS 11429, DOI: 10.1007/978-3-030-17502-3_8.
-
Exploiting Pointer Analysis in Memory Models for Deductive Verification.
Quentin Bouillaguet, Francois Bobot, Mihaela Sighireanu and Boris Yakobowski
Proceedings of VMCAI'19,
LNCS 11388, DOI: 10.1007/978-3-030-11245-5_8.
-
A Verified Implementation of the Bounded List Container.
Raphael Cauderlier, Mihaela Sighireanu.
Proceedings of TACAS'18,
LNCS 10805, DOI: 10.1007/978-3-319-89960-2_10
-
A refinement hierarchy for free list memory allocators.
Bin Fang and Mihaela Sighireanu.
Proceedings of ISMM'17,
IEEE, 2017.
-
SPEN: A Solver for Separation Logic.
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomas Vojnar.
Proceedings of NFM'17,
LNCS 10227, Springer, June 2017.
-
Hierarchical Shape Abstraction for Analysis of Free List Memory Allocators.
Bin Fang and Mihaela Sighireanu.
Proceedings of LOPSTR'16,
LNCS 10184, Springer, 2016.
-
On Automated Lemma Generation for Separation Logic with Inductive Definitions.
Constantin Enea, Mihaela Sighireanu, and Zilin Wu.
Proceedings of ATVA'15,
LNCS 9364, Springer, 2015.
-
Compositional Entailment Checking for a Fragment of Separation Logic.
Constantin Enea, Ondrej Lengál, Mihaela Sighireanu, and Tomas Vojnar.
Proceedings of APLAS'14,
LNCS 8858, Springer, November 2014.
-
Compositional Invariant Checking for Overlaid and Nested Linked Lists.
Constantin Enea, Vlad Saveluc, and Mihaela Sighireanu,
Proceedings of ESOP'13,
LNCS 7792, Springer, March 2013.
-
Local Shape Analysis for Overlaid Data Structures.
Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu,
Proceedings of SAS'13,
LNCS 7935, Springer, September 2013.
-
Abstract Domains for Automated Reasoning about List-Manipulating Programs with Infinite Data.
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu,
Proceedings of VMCAI'12,
LNCS 7148, Springer, January 2012.
- On Inter-Procedural Analysis of Programs with Lists and Data.
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu,
Proceedings of PLDI'11,
ACM July 2011.
- Guidelines for the Verification of Population Protocols.
Julien Clement, Carole Delporte-Gallet, Hugues Fauconnier, and Mihaela Sighireanu.
Proceedings of ICDCS'11
IEEE July 2011.
- Invariant Synthesis for Programs Manipulating Lists with Unbounded Data.
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, and Mihaela Sighireanu,
Proceedings of CAV'10,
LNCS 6174, Springer, July 2010.
- A Logic-Based Framework for Reasoning about Composite Data Structures.
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, and Mihaela Sighireanu,
Proceedings of Concur'09,
LNCS 5710, Springer, September 2009.
- Simple Algorithm for Simple Timed Games
Y. Abdeddaïm, E. Asarin, and M. Sighireanu,
Proceedings of TIME'09,
(C) IEEE, Brixen, Italy, July 2009.
- Planning Robust Temporal Plans A Comparison Between CBTP and TGA Approaches
Y. Abdeddaïm, E. Asarin, M. Gallien , F. Ingrand, C. Lesire and M. Sighireanu,
Proceedings of ICAPS'07,
(C) IEEE, Providence, Rhode Island, USA, September 2007.
- Rewriting Systems with Data.
A. Bouajjani, P. Habermehl, Y. Jurski, and M. Sighireanu,
Proceedings of FCT'07,
(C) Springer-Verlag, LNCS 4639,
Budapest (Hungary), August 2007.
- SPADE: Verification of Multithreaded Dynamic and Recursive Programs.
G. Patin, M. Sighireanu, and T. Touili,
Proceedings of CAV'07,
(C) Springer-Verlag, LNCS 4590,
Berlin (Germany), July 2007.
- A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
A. Bouajjani, Y. Jurski, and M. Sighireanu,
Proceedings of TACAS'07,
(C) Springer-Verlag, LNCS 4424,
Lisbone (Portugal), March 2007.
- Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism
M. Sighireanu, T. Touili,
Proceedings of Infinity Workshop,
Bonn (Germany), August 2006.
- Synthesis and verification of constraints in the PGM protocol
M. Boyer and M. Sighireanu,
Proceedings of the Formal Methods (FM'03),
(C) Springer-Verlag,
Pisa (Italy), September 2003.
- An algorithm for automatically obtaining distributed and fault-tolerant static schedules
A. Girault, H. Kalla, M. Sighireanu, and Y. Sorel
Proceedings of the International Conference on Dependable Systems and Networks (DSN'03)
San-Francisco (USA), June 2003
- Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX
A. Collomb-Annichini and M. Sighireanu,
Proceedings of the Real-Time Tools Workshop (RT TOOLS'01),
Aalborg (Denmark), August 2001.
- TReX: A Tool for Reachability Analysis of Complex Systems
A. Annichini, A. Bouajjani, and M. Sighireanu,
Proceedings of the 13th Intern. Conf. on Computer Aided Verification (CAV'01),
LNCS 2102 (C) Springer-Verlag, Paris (France), July 2001.
- Analyzing Fair Parametric Extended Automata
A. Bouajjani, A. Collomb-Annichini, Y. Lakhnech, and M. Sighireanu,
Proceedings of the 8th Intern. Static Analysis Symposium (SAS'01),
LNCS 2126 (C) Springer-Verlag, Paris (France), July 2001.
- Generation of Fault-Tolerant Static Scheduling for Real-Time Distributed Embedded Systems with Multi-Point Links
A. Girault, C. Lavarenne, M. Sighireanu, and Y. Sorel,
Proceedings of the IEEE Workshop on Fault-Tolerant Parallel
and Distributed Systems, FTPDS'01, (San Francisco, USA), April
2001 (abstract)
- Fault-Tolerant Static Scheduling for Real-Time Distributed Embedded Systems
A. Girault, C. Lavarenne, M. Sighireanu, and Y. Sorel, Proceedings of the 21st International Conference on Distributed Computing Systems, ICDCS'01, (Phoenix, USA), April 2001
- Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus
R. Mateescu and M. Sighireanu, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 (Berlin, Germany), April 2000
- A Graphical Parallel Composition Operator for Process Algebras
H. Garavel and M. Sighireanu, Joint International Conference on
Formal Description Techniques for Distributed Systems and Communication
Protocols, and Protocol Specification, Testing, and Verification, FORTE/PSTV'99,
October 1999, RPC
- Towards a Second Generation of Formal Description Techniques - Rationale for the Design of E-LOTOS
H. Garavel and M. Sighireanu, 3rd International Workshop on Formal Methods for Industrial Critical Systems FMICS'98, May 1998, Amsterdam, The Netherlands
- Model-Checking Verification of the LOTOS Descriptions of the Invoicing Case Study
M. Sighireanu, International Workshop on Comparing System Specification Techniques, March 1998, Nantes, France
- Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS
M. Sighireanu and R. Mateescu, 2nd International Workshop on Applied
Formal Methods in System Design, COST 247, June 1997, Zagreb, Croatia
- CADP'97 - Status, Applications and Perspectives.
H. Garavel, M. Jorgensen, R. Mateescu, C. Pecheur, M. Sighireanu and B. Vivien, Proceedings of the 2nd COST 247 International Workshop on Applied Formal Methods in System Design, Zagreb, Croatia, June 1997.
- On the Introduction of Exceptions in LOTOS
H. Garavel and M. Sighireanu, Joint International Conference on
Formal Description Techniques for Distributed Systems and Communication
Protocols, and Protocol Specification, Testing, and Verification, FORTE/PSTV'96,
October 1996, Kaiserslautern, Germany
- CADP A Protocol Validation and Verification Toolbox
J.C. Fernandez, H. Garavel, A. Kerbrat, L. Mounier, R. Mateescu, and
M. Sighireanu, 8th Conference on Computer-Aided Verification, CAV'96,
August 1996, New Brunswick, New Jersey, USA
Research Reports
- Specification of UNIX Utilities
Nicolas Jeannerod, Yann Regis-Giannas, Claude Marche, Mihaela Sighireanu and Ralf Treinen.
HAL Archives Ouvertes link.
- Simple Algorithm for Simple Timed Game
A. Abdeddaim, E. Asarin, and M. Sighireanu,
HAL preprint hal-00374700, Mai 2008.
- A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes
A. Bouajjani, Y. Jurski, and M. Sighireanu,
LIAFA Research Report RR-0701, January 2007.
- Generation of distributed fault tolerant code for automatically distributed real-time embedded systems
A. Girault, C. Lavarenne, M. Sighireanu, and Y. Sorel,
INRIA Research Report RR-4006, September 2000.
- Requirement Capture, Formal Description and Verification of an Invoicing System
M. Sighireanu and K. J. Turner, INRIA report RR-3575, December 1998
- Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS
M. Sighireanu and R. Mateescu, INRIA report RR-3172, May 1997
ISO Reports (Contributions to the design of E-LOTOS)
- Defect Report on ISO-8807
H. Garavel and M. Sighireanu, ISO report, September 1995
- Towards a proposal for data types in E-LOTOS
A. Jeffrey, H. Garavel, G. Leduc, C. Pecheur, and M. Sighireanu, ISO report, October 1995
- Defect report concerning IS8807 and proposal for a correct flattening of LOTOS parameterized types
H. Garavel and M. Sighireanu, ISO report, October 1995
- Application of the proposed E-LOTOS data type language to the description of OSI and ODP standards
H. Garavel and M. Sighireanu, ISO report, December 1995
- French-Romanian comments regarding some proposed features for E-LOTOS data types
H. Garavel and M. Sighireanu, ISO report, December 1995
- A Proposal for the data type part of E-LOTOS applicable to the formal description of OSI and ODP standards
H. Garavel and M. Sighireanu, ISO report, December 1995
- Position statement regarding E-LOTOS user language
H. Garavel and M. Sighireanu, ISO report, May 1996
- French-Romanian integrated proposal for the user language of E-LOTOS
H. Garavel and M. Sighireanu, ISO report, May 1996
- E-LOTOS user language
M. Sighireanu and H. Garavel, ISO report, October 1996
- On the definition of Modular E-LOTOS
M. Sighireanu and H. Garavel, ISO report, December 1996
- A proposal for co-routines and suspend/resume
H. Garavel and M. Sighireanu, ISO report, December 1996
- A proposal for coroutines in E-LOTOS
H. Garavel and M. Sighireanu, ISO report, July 1997
Thesis
Last modified: Wed Feb 13 2020