2026

Communication dans un congrès

ref_biblio

Lucas Bueri, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu. The Entailment Problem for Separation Logic with Overlaid Structures. 51st International Symposium on Mathematical Foundations of Computer Science, MFCS 2026, Aug 2026, Paris, France. ⟨hal-05671037v2⟩

Accès au texte intégral et bibtex

2025

Communication dans un congrès

ref_biblio

Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu. Deciding Satisfiability for Overlaid Symbolic Heaps. FROCOS 2025 - 15th International Symposium on Frontiers of Combining Systems, Sep 2025, Reykjavik, Iceland. ⟨hal-05143101v3⟩

Accès au texte intégral et bibtex

2024

Communication dans un congrès

ref_biblio

Tanguy Bozec, Nicolas Peltier, Quentin Petitjean, Mihaela Sighireanu. What Is Decidable in Separation Logic Beyond Progress, Connectivity and Establishment?. IJCAR 2024 - 12th International Joint Conference on Automated Reasoning, Jul 2024, Nancy, France. pp.157-175, ⟨10.1007/978-3-031-63501-4_9⟩. ⟨hal-04645164⟩

Accès au texte intégral et bibtex

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Pré-publication, Document de travail

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

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

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

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

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

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

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

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

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

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

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

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

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

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