MOVE : Modélisation et Vérification

Mots clés

Vérification : Model-Checking, Synthèse, Robustesse ; Automates et leurs extensions : Transducteurs, Ordre supérieur, Automates quantitatifs, Automates probabilistes, Automates temporisés, Systèmes d’addition de vecteurs ; Logique : Logique monadique, Logiques temporelles ; Sécurité : Réécriture, Contrôle d’accès, Calculs de processus.

 

Responsable

Pierre-Alain REYNIER

 
Membres

BAUDRU Nicolas  Enseignant-Chercheur / Chercheur
BERTOLISSI Clara  Enseignant-Chercheur / Chercheur
EXIBARD Leo  Doctorant
FRATANI Severine  Enseignant-Chercheur / Chercheur
LOPEZ Theodore  Doctorant
LUGIEZ Denis  Enseignant-Chercheur / Chercheur
MONMEGE Benjamin  Enseignant-Chercheur / Chercheur
MORIN Remi  Enseignant-Chercheur / Chercheur
REYNIER Pierre-Alain  Enseignant-Chercheur / Chercheur
TALBOT Jean-Marc  Enseignant-Chercheur / Chercheur


 

Objectif scientifique

L’équipe MOVE (Modélisation et Vérification), localisée sur le campus de Luminy, s’intéresse au développement de techniques de vérification formelle pour les systèmes logiciels. Plus précisément, l’équipe travaille sur les fondements théoriques de ces outils, et en particulier les approches fondées sur les automates et la logique, comme le model-checking et la synthèse. Ces travaux consistent à étudier différentes extensions de ces modèles sous les perspectives de l’expressivité, de la décidabilité et de questions algorithmiques. Par ailleurs, l’équipe travaille également à l’utilisation de méthodes formelles dans le domaine de la sécurité des systèmes informatiques en utilisant des outils comme la réécriture et les calculs de processus.Le projet scientifique de l’équipe est ainsi organisé selon trois axes :

  1. Langages et transformations : cet axe regroupe les activités en lien avec l’étude des modèles sous-jacents aux techniques de vérification.
  2. Techniques symboliques pour la vérification : cet axe correspond aux travaux algorithmiques en lien principalement avec les problèmes de model-checking et de synthèse.
  3. Sécurité : cet axe regroupe les travaux concernant le développement et l’utilisation de méthodes formelles pour des questions de sécurité, comme le contrôle d’accès ou la vérification de propriétés de protocoles cryptographiques.

 

Publications récentes de l’équipe



38 documents

Article dans une revue

  • Severine Fratani, El Makki Voundy. Epsilon-reducible context-free languages and characterizations of indexed languages. Information and Computation, Elsevier, 2019, 269, pp.104444. ⟨10.1016/j.ic.2019.104444⟩. ⟨hal-02413392⟩
  • Nicolas Baudru, Severine Fratani. On exteriority notions in book embeddings and treewidth. Discrete Mathematics, Elsevier, 2019, pp.111703. ⟨10.1016/j.disc.2019.111703⟩. ⟨hal-02401981⟩
  • Emmanuel Filiot, Olivier Gauwin, Pierre-Alain Reynier, Frédéric Servais. Streamability of nested word transductions. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2019. ⟨hal-02103898⟩
  • Serge Haddad, Benjamin Monmege. Interval Iteration Algorithm for MDPs and IMDPs. Theoretical Computer Science, Elsevier, 2018, 735, pp.111 - 131. ⟨10.1016/j.tcs.2016.12.003⟩. ⟨hal-01809094⟩
  • Luc Dartois, Ismaël Jecker, Pierre-Alain Reynier. Aperiodic String Transducers. International Journal of Foundations of Computer Science, World Scientific Publishing, 2018. ⟨hal-02003676⟩
  • Paul Gastin, Benjamin Monmege. A Unifying Survey on Weighted Logics and Weighted Automata: Core Weighted Logic: Minimal and Versatile Specification of Quantitative Properties. Soft Computing, Springer Verlag, 2018, 22 (4), pp.1047-1065. ⟨10.1007/s00500-015-1952-6⟩. ⟨hal-01130216v2⟩
  • Emmanuel Filiot, Jean-François Raskin, Pierre-Alain Reynier, Frédéric Servais, Jean-Marc Talbot. Visibly pushdown transducers. Journal of Computer and System Sciences, Elsevier, 2018, 97, pp.147-181. ⟨10.1016/j.jcss.2018.05.002⟩. ⟨hal-02093318⟩
  • Emmanuel Filiot, Sebastian Maneth, Pierre-Alain Reynier, Jean-Marc Talbot. Decision problems of tree transducers with origin. Information and Computation, Elsevier, 2018, 261, pp.311-335. ⟨10.1016/j.ic.2018.02.011⟩. ⟨hal-02093317⟩
  • Alexis Bonnecaze, Stéphane Ballet, Nicolas Baudru, Mila Tukumuli. On the construction of the asymmetric Chudnovsky multiplication algorithm in finite fields without derivated evaluation. Comptes Rendus Mathématique, Elsevier Masson, 2017, 355 (7), pp.729 - 733. ⟨10.1016/j.crma.2017.06.002⟩. ⟨hal-01705865⟩
  • Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Benjamin Monmege. Pseudopolynomial iterative algorithm to solve total-payoff games and min-cost reachability games. Acta Informatica, Springer Verlag, 2017, Special Issue: Selected papers from the 26th International Conference on Concurrency Theory (CONCUR 2015), 54 (1), pp.85--125. ⟨10.1007/s00236-016-0276-z⟩. ⟨hal-01414114⟩

Communication dans un congrès

  • Thomas Brihaye, Gilles Geeraerts, Marion Hallet, Benjamin Monmege, Bruno Quoitin. Dynamics on Games: Simulation-Based Techniques and Applications to Routing. 39th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2019), Dec 2019, Bombay, India. ⟨10.4230/LIPIcs.FSTTCS.2019.35⟩. ⟨hal-02414987⟩
  • Pierre-Alain Reynier, Frédéric Servais. On the computation of the minimal coverability set of Petri nets. 13th International Conference on Reachability Problems, Sep 2019, Bruxelles, Belgium. ⟨hal-02442611⟩
  • Léo Exibard, Emmanuel Filiot, Pierre-Alain Reynier. Synthesis of Data Word Transducers. CONCUR 2019, Aug 2019, Amsterdam, Netherlands. ⟨10.4230/LIPIcs.CONCUR.2019.24⟩. ⟨hal-02439660⟩
  • Théodore Lopez, Benjamin Monmege, Jean-Marc Talbot. Determinisation of Finitely-Ambiguous Copyless Cost Register Automata. 44th International Symposium on Mathematical Foundations of Computer Science, Aug 2019, Aachen, Germany. ⟨10.4230/LIPIcs.MFCS.2019.75⟩. ⟨hal-02268107⟩
  • Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier, Ocan Sankur. Robust Controller Synthesis in Timed Büchi Automata: A Symbolic Approach. CAV 2019 - 31st International Conference on Computer Aided Verification, Jul 2019, New-York, United States. pp.572-590, ⟨10.1007/978-3-030-25540-4_33⟩. ⟨hal-02264083⟩
  • Pierre-Alain Reynier, Didier Villevalois. Sequentiality of String-to-Context Transducers. 46th International Colloquium on Automata, Languages, and Programming, Jul 2019, Patras, Greece. ⟨10.4230/LIPIcs.ICALP.2019.123⟩. ⟨hal-02436585⟩
  • Clara Bertolissi, Jerry den Hartog, Nicola Zannone. Using Provenance for Secure Data Fusion in Cooperative Systems. the 24th ACM Symposium SACMAT, Jun 2019, Toronto ON, France. pp.185-194, ⟨10.1145/3322431.3325100⟩. ⟨hal-02440487⟩
  • Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier. Symbolic Approximation of Weighted Timed Games. 38th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2018), Dec 2018, Ahmedabad, India. ⟨10.4230/LIPIcs.FSTTCS.2018.28⟩. ⟨hal-02014051⟩
  • Thomas Brihaye, Arthur Milchior, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege. Efficient algorithms and tools for MITL model-checking and synthesis. 23rd International Conference on Engineering of Complex Computer Systems (ICECCS), Dec 2018, Melbourne, Australia. ⟨hal-02014073⟩
  • Léo Exibard, Emmanuel Filiot, Ismaël Jecker. The Complexity of Transducer Synthesis from Multi-Sequential Specifications. MFCS 2018, Aug 2018, Liverpool, United Kingdom. ⟨10.4230/LIPIcs.MFCS.2018.46⟩. ⟨hal-02134273⟩
  • Nicolas Baudru, Pierre-Alain Reynier. From Two-Way Transducers to Regular Function Expressions. 22nd International Conference on Developments in Language Theory (DLT 2018), Sep 2018, Tokyo, Japan. pp.96-108, ⟨10.1007/978-3-319-98654-8_8⟩. ⟨hal-02003430⟩
  • Giovanni Bacci, Patricia Bouyer, Uli Fahrenberg, Kim Guldstrand Larsen, Nicolas Markey, et al.. Optimal and Robust Controller Synthesis: Using Energy Timed Automata with Uncertainty. FM 2018 - International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.203-221, ⟨10.1007/978-3-319-95582-7_12⟩. ⟨hal-01889222⟩
  • Clara Bertolissi, Daniel Ricardo dos Santos, Silvio Ranise. Solving Multi-Objective Workflow Satisfiability Problems with Optimization Modulo Theories Techniques.. SACMAT, Jun 2018, Indianapolis IN, United States. ⟨hal-02092833⟩
  • Clara Bertolissi, Omar Boucelma, Worachet Uttha. Enhancing Security in the Cloud: when Traceability meets Access Control. The 12th International Conference for Internet Technology and Secured Transactions ICITST 2017, Dec 2017, Cambridge, United Kingdom. ⟨hal-01787036⟩
  • Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege. Timed-Automata-Based Verification of MITL over Signals. 24th International Symposium on Temporal Representation and Reasoning (TIME 2017), Oct 2017, Mons, France. pp.7:1--7:19, ⟨10.4230/LIPIcs.TIME.2017.7⟩. ⟨hal-01526986⟩
  • Emmanuel Filiot, Pierre-Alain Reynier. Copyful Streaming String Transducers. 11th International Workshop on Reachability Problems (RP 2017), Sep 2017, London, United Kingdom. ⟨hal-01782442⟩
  • Thomas Brihaye, Gilles Geeraerts, Hsi-Ming Ho, Benjamin Monmege. MightyL: A Compositional Translation from MITL to Timed Automata. 29th International Conference on Computer Aided Verification (CAV'17), Jul 2017, Heidelberg, Germany. pp.421-440, ⟨10.1007/978-3-319-63387-9_21⟩. ⟨hal-01525524⟩
  • Laure Daviaud, Ismaël Jecker, Pierre-Alain Reynier, Didier Villevalois. Degree of sequentiality of weighted automata. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS 2017), Apr 2017, Uppsala, Sweden. ⟨hal-01782446⟩
  • Damien Busatto-Gaston, Benjamin Monmege, Pierre-Alain Reynier. Optimal Reachability in Divergent Weighted Timed Games. 20th International Conference on Foundations of Software Science and Computation Structures (FoSSaCS'17), Apr 2017, Uppsala, Sweden. pp.162-178, ⟨10.1007/978-3-662-54458-7_10⟩. ⟨hal-01522546⟩
  • Luc Dartois, Ismaël Jecker, Pierre-Alain Reynier. Aperiodic String Transducers. Proc. 20th International Conference on Developments in Language Theory (DLT 2016), 2016, Unknown, Unknown Region. pp.125-137, ⟨10.1007/978-3-662-53132-7_11⟩. ⟨hal-01475444⟩
  • Laure Daviaud, Pierre-Alain Reynier, Jean-Marc Talbot. A Generalized Twinning Property for Minimisation of Cost Register Automata. Proc. 31st Annual ACM/IEEE Symposium on Logic in Computer Science (LICS'16), 2016, Unknown, Unknown Region. pp.857--866, ⟨10.1145/2933575.2934549⟩. ⟨hal-01475441⟩
  • Stéphanie Delaune, Pascal Lafourcade, Denis Lugiez, Ralf Treinen. Symbolic Protocol Analysis in Presence of a Homomorphism Operator and Exclusive Or. Automata, Languages and Programming, 33rd International Colloquium, , Jul 2006, Venise, Italy. ⟨hal-01759947⟩

Chapitre d'ouvrage

  • Luc Dartois, Emmanuel Filiot, Jean-Marc Talbot. Two-Way Parikh Automata with a Visibly Pushdown Stack. Bojańczyk M., Simpson A. Foundations of Software Science and Computation Structures. FoSSaCS 2019, Springer, pp.189-206, 2019, 978-3-030-17126-1. ⟨10.1007/978-3-030-17127-8_11⟩. ⟨hal-02162279⟩

Direction d'ouvrage, Proceedings

  • Igor Potapov, Pierre-Alain Reynier. Reachability Problems: 12th International Conference, RP 2018, Marseille, France, September 24-26, 2018, Proceedings. 11123 (1), Springer, 2018, Theoretical Computer Science and General Issues, 978-3-030-00249-7. ⟨hal-02126180⟩

Pré-publication, Document de travail

  • Thomas Brihaye, Gilles Geeraerts, Axel Haddad, Engel Lefaucheux, Benjamin Monmege. One-Clock Priced Timed Games with Arbitrary Weights. 2019. ⟨hal-02424743⟩

Thèse

  • Damien Busatto-Gaston. Symbolic controller synthesis for timed systems: robustness and optimality. Computer Science and Game Theory [cs.GT]. Aix Marseille Université, 2019. English. ⟨tel-02436831⟩
  • Didier Villevalois. Simplifying Transducers using Sequentiality. Formal Languages and Automata Theory [cs.FL]. Aix-Marseille Université (AMU), 2019. English. ⟨tel-02436759⟩
  • El Makki Voundy. Langages epsilon-sûrs et caractérisations des langages d'ordres supérieurs. Informatique et langage [cs.CL]. Aix-Marseille Université, 2017. Français. ⟨tel-02453297⟩