Publications HAL

2022

Article dans une revue

ref_biblio
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, et al.. The CoLiS Platform for the Analysis of Maintainer Scripts in Debian Software Packages. International Journal on Software Tools for Technology Transfer, 2022. ⟨hal-03737886⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03737886/file/main.pdf BibTex

2020

Communication dans un congrès

ref_biblio
Benedikt Becker, Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, et al.. Analysing installation scenarios of Debian packages. TACAS 2020 - 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, Apr 2020, The conference took place on-line, because it couldn't be held in Dublin, Ireland. pp.235-253, ⟨10.1007/978-3-030-45237-7_14⟩. ⟨hal-02355602v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02355602/file/main.pdf BibTex

2019

Communication dans un congrès

ref_biblio
Ezio Bartocci, Dirk Beyer, Paul Black, Grigory Fedyukovich, Hubert Garavel, et al.. TOOLympics 2019: An Overview of Competitions in Formal Methods. 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Apr 2019, Prague, Czech Republic. pp.3-24, ⟨10.1007/978-3-030-17502-3_1⟩. ⟨hal-02094030⟩
Accès au bibtex
BibTex
ref_biblio
Mihaela Sighireanu, Juan Navarro Pérez, Andrey Rybalchenko, Nikos Gorogiannis, Radu Iosif, et al.. SL-COMP: Competition of Solvers for Separation Logic. Tools and Algorithms for the Construction and Analysis of Systems - 25 Years of {TACAS:} TOOLympics, Held as Part of {ETAPS} 2019, Apr 2019, Prague, Czech Republic. pp.116-132, ⟨10.1007/978-3-030-17502-3_8⟩. ⟨hal-02388022⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02388022/file/main.pdf BibTex

Rapport

ref_biblio
Nicolas Jeannerod, Claude Marché, Yann Régis-Gianas, Mihaela Sighireanu, Ralf Treinen. Specification of UNIX Utilities. [Technical Report] ANR. 2019. ⟨hal-02321691⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02321691/file/main.pdf BibTex

2018

Communication dans un congrès

ref_biblio
Raphaël Cauderlier, Mihaela Sighireanu. A Verified Implementation of the Bounded List Container. TACAS, Apr 2018, Thessaloniki, Greece. pp.172-189, ⟨10.1007/978-3-319-89960-2_10⟩. ⟨hal-04425550⟩
Accès au bibtex
BibTex
ref_biblio
Quentin Bouillaguet, François Bobot, Mihaela Sighireanu, Boris Yakobowski. A Value-based Memory Model for Deductive Verification. Les vingt-neuvièmes Journées Francophones des Langages Applicatifs (The 29th Francophone Days of Application Languages - JFLA 2018), Jan 2018, Banyuls-sur-mer, France. ⟨cea-01809497⟩
Accès au texte intégral et bibtex
https://cea.hal.science/cea-01809497/file/jfla_final.pdf BibTex

2017

Article dans une revue

ref_biblio
Constantin Enea, Ondřej Lengál, Sighireanu Mihaela, Tomáš · Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. Formal Methods in System Design, 2017, 51 (3), pp.575-607. ⟨10.1007/s10703-017-0289-4⟩. ⟨hal-01937818⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01937818/file/main.pdf BibTex

Communication dans un congrès

ref_biblio
Constantin Enea, Ondřej Lengál, Mihaela Sighireanu, Tomáš Vojnar. SPEN: A Solver for Separation Logic. 9th NASA Formal Methods Symposium (NFM 2017), May 2017, Moffett Field, United States. ⟨hal-01936210⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01936210/file/main.pdf BibTex

2015

Pré-publication, Document de travail

ref_biblio
Constantin Enea, Mihaela Sighireanu, Zhilin Wu. On Automated Lemma Generation for Separation Logic with Inductive Definitions. 2015. ⟨hal-01175732⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01175732/file/main_full.pdf BibTex

2012

Rapport

ref_biblio
Constantin Enea, Vlad Saveluc, Mihaela Sighireanu. Compositional Invariant Checking for Overlaid and Nested Linked Lists. [Research Report] 2012, pp.27. ⟨hal-00768389⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-00768389/file/head.pdf BibTex

2011

Communication dans un congrès

ref_biblio
Julien Clément, Carole Delporte-Gallet, Hugues Fauconnier, Mihaela Sighireanu. Mode d'emploi pour la vérification des protocoles de population. 13es Rencontres Francophones sur les Aspects Algorithmiques de Télécommunications (AlgoTel), 2011, Cap Estérel, France. ⟨inria-00584684⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00584684/file/main.pdf BibTex

2010

Autre publication scientifique

ref_biblio
Ahmed Bouajjani, Cezara Dragoi, Constantin Enea, Ahmed Rezine, Mihaela Sighireanu. Invariant Synthesis for Programs Manipulating Lists with Unbounded Data. 2010. ⟨hal-00473754⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00473754/file/inv.pdf BibTex

Rapport

ref_biblio
Julien Clément, Carole Delporte-Gallet, Hugues Fauconnier, Mihaela Sighireanu. Guidelines for Verification of Population Protocols. 2010. ⟨hal-00565090⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00565090/file/main.pdf BibTex

2008

Pré-publication, Document de travail

ref_biblio
Yasmina Abdeddaim, Eugene Asarin, Mihaela Sighireanu. Simple Algorithm for Simple Timed Games. 2008. ⟨hal-00374700v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00374700/file/main_lncs.pdf BibTex

2007

Communication dans un congrès

ref_biblio
Yasmina Abdeddaim, Eugene Asarin, Matthieu Gallien, Félix Ingrand, Charles Lesire, et al.. Planning Robust Temporal Plans A Comparison Between CBTP and TGA Approaches. International Conference on Automated Planning and Scheduling, Sep 2007, Providence, Rhode Island, United States. pp.2-9. ⟨hal-00157935⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00157935/file/icaps07mg.pdf BibTex
ref_biblio
Ahmed Bouajjani, Peter Habermehl, Yan Jurski, Mihaela Sighireanu. Rewriting Systems with Data. International Symposium on Fundamentals of Computation Theory, Aug 2007, Budapest, Hungary. pp.1-22. ⟨hal-00157782⟩
Accès au bibtex
BibTex
ref_biblio
Gael Patin, Mihaela Sighireanu, Tayssir Touili. SPADE: Verification of Multithreaded Dynamic and Recursive Programs. 19th International Conference in Computer Aided Verification, Jul 2007, Berlin, Germany. pp.254-257. ⟨hal-00160449⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00160449/file/main.pdf BibTex
ref_biblio
Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu. A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes. Mar 2007, pp.690-705. ⟨hal-00129014⟩
Accès au bibtex
BibTex

2006

Communication dans un congrès

ref_biblio
Mihaela Sighireanu, Tayssir Touili. Bounded Communication Reachability Analysis of Process Rewrite Systems with Ordered Parallelism. Infinity, 2006, Bonn, Germany. ⟨hal-00110134⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00110134/file/main.pdf BibTex

Chapitre d'ouvrage

ref_biblio
Kenneth J. Turner, Mihaela Sighireanu. 6 (E-)LOTOS: (Enhanced) Language Of Temporal Ordering Specification. H. Habrias and M. Frappier. Software Specification Methods -- An Overview Using a Case Study, ISTE Hermes & Lavoisier, pp.233-258, 2006. ⟨hal-00160467⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00160467/file/lotos.pdf BibTex

Pré-publication, Document de travail

ref_biblio
Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu. A Generic Framework for Reasoning about Dynamic Networks of Infinite-State Processes. 2006. ⟨hal-00129018⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00129018/file/BJS07a-full.pdf BibTex
ref_biblio
Ahmed Bouajjani, Yan Jurski, Mihaela Sighireanu. Reasoning about Dynamic Networks of Infinite-State Processes with Global Synchronization. 2006. ⟨hal-00129025⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00129025/file/BJS07b-full.pdf BibTex

2003

Article dans une revue

ref_biblio
Radu Mateescu, Mihaela Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. Science of Computer Programming, 2003, 46(3), pp.255-281. ⟨10.1016/s0167-6423(02)00094-1⟩. ⟨hal-00109620⟩
Accès au bibtex
BibTex

Communication dans un congrès

ref_biblio
Marc Boyer, Mihaela Sighireanu. Synthesis and verification of constraints in the PGM protocol. 12th International Formal Methods Europe Symposium, FM'03, Sep 2003, Pisa, Italy. pp.264-281. ⟨hal-00110252⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00110252/file/main.pdf BibTex
ref_biblio
Alain Girault, Hamoudi Kalla, Mihaela Sighireanu, Yves Sorel. An algorithm for automatically obtaining distributed and fault-tolerant static schedules. Jun 2003, pp.165-190. ⟨hal-00110453⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00110453/file/main.pdf BibTex

2001

Communication dans un congrès

ref_biblio
Aurore Collomb-Annichini, Mihaela Sighireanu. Parameterized Reachability Analysis of the IEEE 1394 Root Contention Protocol using TReX. Proceedings of the Real-Time Tools Workshop (RT TOOLS'01), Aug 2001, Aalborg, Denmark. pp.1-20. ⟨hal-00110454⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00110454/file/ieee1394rc.pdf BibTex
ref_biblio
Aurore Collomb-Annichini, Ahmed Bouajjani, Mihaela Sighireanu. TReX: A Tool for Reachability Analysis of Complex Systems. Jul 2001, pp.368-372. ⟨hal-00110460⟩
Accès au bibtex
BibTex
ref_biblio
Ahmed Bouajjani, Aurore Collomb-Annichini, Yassine Lakhnech, Mihaela Sighireanu. Analyzing Fair Parametric Extended Automata. 2001, pp.335--355. ⟨hal-00129051⟩
Accès au bibtex
BibTex

Chapitre d'ouvrage

ref_biblio
Guy Leduc, Alan Jeffrey, Mihaela Sighireanu. Introduction à E-LOTOS. Ana Cavalli. Ingenierie des protocoles et qualite de service, Hermes Lavoisier, pp.213-252, 2001, serie IC2. ⟨hal-00109629⟩
Accès au texte intégral et bibtex
https://hal.science/hal-00109629/file/ELOTOS.pdf BibTex

2000

Rapport

ref_biblio
Radu Mateescu, Mihaela Sighireanu. Efficient On-the-Fly Model-Checking for Regular Alternation-Free Mu-Calculus. [Research Report] RR-3899, INRIA. 2000. ⟨inria-00072755⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072755/file/RR-3899.pdf BibTex
ref_biblio
Alain Girault, Christophe Lavarenne, Mihaela Sighireanu, Yves Sorel. Fault-Tolerant Static Scheduling for Real-Time Distributed Embedded Systems. [Research Report] RR-4006, INRIA. 2000. ⟨inria-00072638⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00072638/file/RR-4006.pdf BibTex

1998

Article dans une revue

ref_biblio
Mihaela Sighireanu, Radu Mateescu. Verification of the Link Layer Protocol of the IEEE-1394 Serial Bus (``FireWire''): an Experiment with E-LOTOS. International Journal on Software Tools for Technology Transfer, 1998, 2(1), pp.68-88. ⟨10.1007/s100090050018⟩. ⟨hal-00109622⟩
Accès au bibtex
BibTex

Rapport

ref_biblio
Mihaela Sighireanu, Kenneth J. Turner. Requirement Capture, Formal Description and Verification of an Invoicing System. RR-3575, INRIA. 1998. ⟨inria-00073106⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073106/file/RR-3575.pdf BibTex

1997

Rapport

ref_biblio
Mihaela Sighireanu, Radu Mateescu. Validation of the Link Layer Protocol of the IEEE-1394 Serial Bus («FireWire»): an Experiment with E-LOTOS. [Research Report] RR-3172, INRIA. 1997. ⟨inria-00073516⟩
Accès au texte intégral et bibtex
https://inria.hal.science/inria-00073516/file/RR-3172.pdf BibTex