Researcher identifiers

Number of documents

68

Pascale Le Gall


Professeur en Informatique, CentraleSupélec, CNU 27, laboratoire MICS


Journal articles14 documents

  • J.-C. Léchenet, N. Kosmatov, P. Le Gall. Cut branches before looking for bugs: certifiably sound verification on relaxed slices. Formal Aspects of Computing, 2018, 30 (1), pp.107-131. ⟨10.1007/s00165-017-0439-x⟩. ⟨cea-01801601⟩
  • L. Blatter, N. Kosmatov, P. Le Gall, V. Prevosto. RPP: Automatic proof of relational properties by self-composition. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2017, 10205 LNCS, pp.391-397. ⟨10.1007/978-3-662-54577-5_22⟩. ⟨cea-01808885⟩
  • I. Boudhiba, C. Gaston, P. Le Gall, V. Prevosto. Symbolic execution of transition systems with function summaries. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2017, 10375 LNCS, pp.41-58. ⟨10.1007/978-3-319-61467-0_3⟩. ⟨cea-01808888⟩
  • J.-C. Léchenet, N. Kosmatov, P. Le Gall. Cut branches before looking for bugs: Sound verification on relaxed slices. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2016, 9633, pp.179-196. ⟨10.1007/978-3-662-49665-7_11⟩. ⟨cea-01808894⟩
  • Marc Aiguier, Agnès Arnould, Pascale Le Gall, Delphine Longuet. Exhaustive test sets for algebraic specification correctness. Journal of Software Testing, Verification, and Reliability, John Wiley & Sons, 2016, 26 (4), pp.294-317. ⟨http://onlinelibrary.wiley.com/doi/10.1002/stvr.1598/abstract⟩. ⟨10.1002/stvr.1598 ⟩. ⟨hal-01318362⟩
  • Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini. Étude de réseaux de Thomas par validation de propriétés LTL pour Pseudomonas aeruginosa. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2015, 34 (5), pp.575 - 600. ⟨10.3166/TSI.34.575-600⟩. ⟨hal-01819818⟩
  • Mbarka Mabrouki, Marc Aiguier, Jean-Paul Comet, Pascale Le Gall, Adrien Richard. Embedding of biological regulatory networks and property preservation. Mathematics in Computer Science, Springer, 2011, 5 (1), pp.263-288. ⟨hal-00782867⟩
  • Mathieu Poudret, Thomas Bellet, Agnès Arnould, Pascale Le Gall. Transformations de graphes pour les opérations topologiques en modélisation géométrique. Revue Electronique Francophone d'Informatique Graphique, Association Française d'Informatique Graphique, 2010, 4 (1), http://www.irit.fr/REFIG/index.php/refig/article/view/77. ⟨http://www.irit.fr/REFIG/index.php/refig/article/view/77⟩. ⟨hal-01137358⟩
  • Delphine Longuet, Marc Aiguier, Pascale Le Gall. Proof-Guided Test Selection from First-Order Specifications with Equality. Journal of Automated Reasoning, Springer Verlag, 2010, 45 (4), pp.437-473. ⟨hal-00782871⟩
  • Marc Aiguier, Pascale Le Gall, Mbarka Mabrouki. Complex software systems : Formalization and Applications. International Journal On Advances in Software, IARIA, 2009, 2 (1), pp.47-62. ⟨hal-00782879⟩
  • Mathieu Poudret, Agnès Arnould, Jean-Paul Comet, Pascale Le Gall, Philippe Meseure, et al.. Topology-based Abstraction of Complex Biologiical Systems: Application to the Golgi Apparatus. Theorie in den Biowissenschaften / Theory in Biosciences, Springer Verlag, 2008, 127 (2), pp.79-88. ⟨hal-00352003⟩
  • Daniel Mateus, Jean-Pierre Gallois, Jean-Paul Comet, Pascale Le Gall. Symbolic modeling of genetic regulatory networks. Journal of Bioinformatics and Computational Biology, World Scientific Publishing, 2007, 5 (2B), pp.627-640. ⟨hal-00293530⟩
  • Franck Ledoux, Jean-Marc Mota, Agnès Arnould, Catherine Dubois, Pascale Le Gall, et al.. Spécifications formelles du chanfreinage. Techniques et Sciences Informatiquess, Editions Hermès, 2002, 21 (8), pp.1-26. ⟨hal-00352083⟩
  • Agnès Arnould, Pascale Le Gall. Test de conformité : une approche algébrique. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2002, 21 (9), pp.1219-1242. ⟨hal-00352131⟩

Conference papers41 documents

  • Virgile Robles, Nikolai Kosmatov, Virgile Prévosto, Louis Rilling, Pascale Le Gall. MetAcsl: Specification and Verification of High-Level Properties. TACAS 2019, Apr 2019, Prague, Czech Republic. ⟨cea-02019790⟩
  • Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prévosto. RPP : Preuve automatique de propriétés relationnelles par Self-Composition. Approches Formelles pour l'Assistance au Développement de Logiciels - AFADL, Jun 2018, Grenoble, France. ⟨cea-01835491⟩
  • Lionel Blatter, Nikolai Kosmatov, Pascale Le Gall, Virgile Prévosto, Guillaume Petiot. Static and Dynamic Verification of Relational Properties on Self-Composed C Code. Tests and Proofs - TAP, Jun 2018, Toulouse, France. ⟨cea-01835470⟩
  • Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prévosto. Symbolic execution of transition systems with function summaries. 11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany. ⟨cea-01810693⟩
  • Thomas Bellet, Agnès Arnould, Hakim Belhaouari, Pascale Le Gall. Geometric Modeling: Consistency Preservation Using Two-Layered Variable Substitutions. Graph Transformation: 10th International Conference, ICGT 2017, Held as Part of STAF 2017, Jul 2017, Marburg, Germany. ⟨hal-01817827⟩
  • Nassim Benharrat, Christophe Gaston, Robert Hierons, Arnault Lapitre, Pascale Gall. Constraint-Based Oracles for Timed Distributed Systems. 29th IFIP International Conference on Testing Software and Systems (ICTSS), Oct 2017, St. Petersburg, Russia. pp.276-292, ⟨10.1007/978-3-319-67549-7_17⟩. ⟨hal-01678964⟩
  • Gabriel Pedroza, Pascale Le Gall, Christophe Gaston, Fabrice Bersey. Timed-model-based Method for Security Analysis and Testing of Smart Grid Systems. 19th International Symposium on Real-Time Distributed Computing (ISORC) 2016, May 2016, York, United Kingdom. ⟨10.1109/isorc.2016.15 ⟩. ⟨cea-01302826⟩
  • Jean-Christophe Léchenet, Nikolai Kosmatov, Pascale Le Gall. Coq a dit : fromage tranché ne peut cacher ses trous *. Vingt-septièmes Journées Francophones des Langages Applicatifs (JFLA 2016), Jan 2016, Saint-Malo, France. ⟨hal-01333605⟩
  • Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prévosto. Model-based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts. The 27th IFIP International Conference on Testing Software and Systems (ICTSS-2015) , Nov 2015, Sharjah and Dubai, United Arab Emirates. ⟨cea-01810689⟩
  • Boutheïna Bannour, Boutheina Bannour, Jose Escobedo, Christophe Gaston, Pascale Le Gall, et al.. Security Weaknesses Detection by Symbolic Analysis of Scenarios. 2014 21st Asia-Pacific Software Engineering Conference (APSEC), Dec 2014, Jeju, France. ⟨10.1109/APSEC.2014.61⟩. ⟨hal-01812121⟩
  • Boutheïna Bannour, Boutheina Bannour, Jose Escobedo, Christophe Gaston, Pascale Le Gall, et al.. Designing Sequence Diagram Models for Robustness to Attacks. 2014 IEEE Seventh International Conference on Software Testing, Verification and Validation Workshops (ICSTW), Mar 2014, OH, France. ⟨10.1109/ICSTW.2014.50⟩. ⟨hal-01812124⟩
  • Hakim Belhaouari, Agnès Arnould, Pascale Le Gall, Thomas Bellet. JERBOA: A Graph Transformation Library for Topology-Based Geometric Modeling. 7th International Conference on Graph Transformation (ICGT 2014), Jul 2014, York, United Kingdom. ⟨hal-01012851⟩
  • Paolo Ballarini, Emmanuelle Gallet, Pascale Le Gall, Matthieu Manceny. Formal Analysis of the Wnt/β-catenin through Statistical Model Checking. 6th International Symposium, ISoLA 2014, Tiziana Margaria, Bernhard Steffen, Oct 2014, Corfu, Greece. ⟨hal-01110747⟩
  • Hakim Belhaouari, Agnès Arnould, Pascale Le Gall, Thomas Bellet. Jerboa : a graph transformation library for topology-base geometric modeling. International Conference on Graph Transformations, Holger Giese, Barbara König, Jul 2014, York, United Kingdom. ⟨hal-01110743⟩
  • Paolo Ballarini, Emmanuelle Gallet, Pascale Le Gall, Matthieu Manceny. Formal analysis of the Wnt/β-catenin pathway through statistical model checking. International Symposium On Leveraging Applications of Formal Methods, Verification and Validation , Oct 2014, Corfu, Greece. ⟨hal-01819866⟩
  • E Gallet, M Manceny, P Le Gall, Paolo Ballarini. An LTL Model Checking Approach for Biological Parameter Inference. International Conference on Formal Engineering Methods, Nov 2014, Luxembourg, Luxembourg. ⟨hal-01819841⟩
  • Emmanuelle Gallet, Matthieu Manceny, Pascale Le Gall, Paolo Ballarini. An LTL Model Checking Approach for Biological Parameter Inference. 16th International Conference on Formal Engineering Methods, Nov 2014, Luxembourg, Luxembourg. ⟨hal-01110746⟩
  • Christophe Gaston, Robert Hierons, Pascale Le Gall. An implementation relation and test framework for timed distributed systems. International Conference on Testing Software and Systems, Nov 2013, Istanbul, Turkey. ⟨cea-01810746⟩
  • Thomas Bellet, Agnès Arnould, Pascale Le Gall. JERBOA : un modeleur géométrique à base de règles. Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Jan 2012, Grenoble, France. ⟨hal-00936743⟩
  • Boutheina Bannour, Jose Escobedo, Christophe Gaston, Pascale Gall. Off-Line Test Case Generation for Timed Symbolic Model-Based Conformance Testing. 24th International Conference on Testing Software and Systems (ICTSS), Nov 2012, Aalborg, Denmark. pp.119-135, ⟨10.1007/978-3-642-34691-0_10⟩. ⟨hal-01482398⟩
  • Thomas Bellet, Agnès Arnould, Pascale Le Gall. Rule-based transformations for geometric modeling. 6th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2011), Part of ETAPS 2011, Apr 2011, Saarbrücken, Germany. 20p. ⟨hal-00865432⟩
  • Thomas Bellet, Mathieu Poudret, Agnès Arnould, Laurent Fuchs, Pascale Le Gall. Designing a Topological Modeler Kernel: A Rule-Based Approach. Shape Modeling International (SMI'10), Jun 2010, Aix-en-Provence, France. ⟨hal-00488171⟩
  • Jose Pablo Escobedo, Christophe Gaston, Pascale Le Gall, Ana Rosa Cavalli. Testing web service orchestrators in context : a symbolic approach. SEFM 2010 : 8th IEEE International Conference on Software Engineering and Formal Methods, Sep 2010, Pisa, Italy. pp.257 - 267, ⟨10.1109/SEFM.2010.30⟩. ⟨hal-01306744⟩
  • Mathieu Poudret, Thomas Bellet, Agnès Arnould, Pascale Le Gall. Transformations de graphes pour les opérations topologiques en modélisation géométrique. 22es Journées de l'Association Francophone d'Informatique Graphique, chapitre français d'Eurographics (AFIG 2009), Nov 2009, Arles, France. ⟨hal-00488533⟩
  • Jose Pablo Escobedo, Christophe Gaston, Pascale Le Gall, Ana Rosa Cavalli. Observability and controllability issues in conformance testing of Web service compositions. TESTCOM/FATES 2009 : 21st IFIP International Conference on Testing of Communicating Systems and 9th International Workshop on Formal Approaches to Testing of Software, Nov 2009, Eindhoven, Netherlands. pp.217 - 222, ⟨10.1007/978-3-642-05031-2_15⟩. ⟨hal-01360755⟩
  • Matthieu Manceny, Marc Aiguier, Pascale Le Gall, Joan Hérisson, Ivan Junier, et al.. Spatial Information and Boolean Genetic Regulatory Networks.. Bioinformatics and Computational Biology (BICoB), Apr 2008, New Orleans, United States. pp.270-281, ⟨10.1007/978-3-642-00727-9_26 ⟩. ⟨hal-00812184⟩
  • Patricia Mouy, Bruno Marre, Nicky Williams, Pascale Le Gall. Generation of All-Paths Unit Test with Function Calls. First International Conference on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, April 9-11, 2008, 2008, Lillehammer, Norway. pp.32--41, ⟨10.1109/ICST.2008.35⟩. ⟨hal-01810199⟩
  • Alain Faivre, Christophe Gaston, Pascale Le Gall, Assia Touil. Testing of Software and Communicating Systems. 20th IFIP TC/WG 6.1 International Conference, TestCom 2008 - 8 th International Workshop, TATES 2008, Jun 2008, Tokyo, Japan. pp.184-199, ⟨10.1007/978-3-540-68524-1⟩. ⟨hal-00289229⟩
  • Mathieu Poudret, Agnès Arnould, Jean-Paul Comet, Pascale Le Gall. Graph Transformation for Topology Modelling..  4th International Conference on Graph Transformation (ICGT'08), Sep 2008, Leicester, United Kingdom. pp.147-161, ⟨10.1007/978-3-540-87405-8_11⟩. ⟨hal-00341176⟩
  • Mathieu Poudret, Jean-Paul Comet, Pascale Le Gall, Agnès Arnould, Philippe Meseure. Topology-based Geometric Modelling for Biological Cellular Processes. International Conference on Language and Automata Theory and Applications, Mar 2007, Tarragone, Spain. pp.497-508. ⟨hal-00348152⟩
  • Mathieu Poudret, Jean-Paul Comet, Pascale Le Gall, François Képès, Agnès Arnould, et al.. Exploring Topological Modelling to Discriminate Models of Golgi Apparatus Dynamics. European Conference on Complex Systems (ECCS), Oct 2007, Dresde, Germany. ⟨hal-00348154⟩
  • Marc Aiguier, Agnès Arnould, Pascale Le Gall, Delphine Longuet. Test selection criteria for quantifier-free first-order specifications. 2nd IPM International Symposium on Fundamentals of Software Engineering (FSEN 2007), Apr 2007, Tehran, Iran. pp.144-159. ⟨hal-00353787⟩
  • Christophe Gaston, Pascale Le Gall, Nicolas Rapin, Assia Touil. Symbolic execution techniques for test purpose definition. Proceedings of the 18th international conference on Testing of Communicating Systems (TestCom), 2006, United States. pp.1--18. ⟨hal-00342082⟩
  • Marc Aiguier, Karim Berkani, Pascale Le Gall. Feature specification and static analysis for interaction resolution. 14th International Symposium on Formal Methods (FM 2006), Aug 2006, Hamilton, Canada. pp.364--379, ⟨10.1007/11813040_25⟩. ⟨hal-00341977⟩
  • Assia Touil, Christophe Gaston, Pascale Le Gall. Automatic generation of symbolic test purposes. Proceedings of the second MoDeVa (Model Design and Validation) workshop, 2005, Jamaica. pp.n.a. ⟨hal-00342173⟩
  • Pascale Le Gall. Testing from Abstract Data Type Specifications. Training And Research On Testing (TAROT) Summer School, 2005, France. pp.n.a. ⟨hal-00342088⟩
  • Hélène Jouve, Pascale Le Gall, Sophie Coudert. An Automatic Off-Line Feature Interaction Detection Method by Static Analysis of Specifications. Proceedings of the 8th International Conference on Feature Interactions in Telecommunications and Software Systems (FIW'05), 2005, United Kingdom. pp.131--146. ⟨hal-00342087⟩
  • Daniel Mateus, Jean-Pierre Gallois, Pascale Le Gall. Evaluation symbolique appliquée à l'étude de réseaux de régulation génétique. Journée Thématique <>, 2005, France. pp.n.a. ⟨hal-00342150⟩
  • Marc Aiguier, Christophe Gaston, Pascale Le Gall, Delphine Longuet, Assia Touil. A Temporal Logic for Input Output Symbolic Transition Systems. 12th Asia-Pacific Software Engineering Conference (APSEC'05), Dec 2005, Taipei, Taiwan. pp.43--50, ⟨10.1109/APSEC.2005.19⟩. ⟨hal-00341980⟩
  • Marc Aiguier, Agnès Arnould, Clément Boin, Pascale Le Gall, Bruno Marre. Testing from algebraic specifications: test data set selection by unfolding axioms. Proceedings of the 5th International Workshop on Formal Approaches to Testing of Software (FATES 2005), 2005, United Kingdom. pp.203--217, ⟨10.1007/11759744_14⟩. ⟨hal-00341964⟩
  • F. Ledoux, Jean-Marc Mota, A. Arnould, Catherine Dubois, P. Le Gall, et al.. Spécifications formelles du chanfreinage. AFADL2001, Jan 2001, X, France. ⟨hal-01124624⟩

Book sections4 documents

  • Imen Boudhiba, Christophe Gaston, Pascale Gall, Virgile Prévosto. Model-based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts. Testing Software and Systems , 9447), pp.35-51, 2014, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-25945-1_3⟩. ⟨hal-01470156⟩
  • C. Gaston, P. Le Gall, N. Rapin, A. Touil. Symbolic Execution-Based Techniques for Conformance Testing. Model‐Driven Engineering for Distributed Real‐Time Systems: MARTE Modeling, Model Transformations and their Usages, John Wiley and Sons, pp.73-103, 2013, 9781848211155. ⟨10.1002/9781118558096.ch4⟩. ⟨cea-01818541⟩
  • Marie-Claude Gaudel, Pascale Le Gall. Testing data types implementations from algebraic specifications. R. Hierons, J. Bowen, and M. Harman. Formal Methods and Testing, Springer-Verlag, pp.209--239, 2008, Lecture Notes in Computer Science, ⟨10.1007/978-3-540-78917-8_7⟩. ⟨hal-00270574⟩
  • Mathieu Poudret, Jean-Paul Comet, Pascale Le Gall, François Képès, Agnès Arnould, et al.. Toward a computer-aided methodology for topology-based simulation of the Golgi apparatus. Proc. of the Lille Spring school on Modelling and simulation of biological processes in the context of genomics, EDP SCIENCES, pp.89--104, 2008. ⟨hal-00353755⟩

Directions of work or proceedings1 document

  • Frédéric Dadeau, Pascale Le Gall. Actes des 14e journées sur les Approches Formelles dans l'Assistance au Développement de Logiciels. Dadeau, Frédéric; Le Gall, Pascale. Approches Formelles dans l'Assistance au Développement de Logiciels, Jun 2015, Bordeaux, France. pp.88, 2015, ⟨http://events.femto-st.fr/afadl-2015⟩. ⟨hal-01155626⟩

Other publications4 documents

  • Christophe Gaston, Pascale Le Gall, Nicolas Rapin, Assia Touil. Generating test case from symbolic transition systems based on constrained unfolding. 2005. ⟨hal-00342083⟩
  • Marc Aiguier, Christophe Gaston, Pascale Le Gall, Delphine Longuet, Assia Touil. A temporal logic for input output symbolic transition systems. 2005. ⟨hal-00341981⟩
  • Marc Aiguier, Agnès Arnould, Clément Boin, Pascale Le Gall, Bruno Marre. Testing from algebraic specifications: test data set selection by unfolding axioms. 2005. ⟨hal-00341963⟩
  • Marc Aiguier, Christophe Gaston, Pascale Le Gall. Feature specification: a logic-independent approach. 2005. ⟨hal-00341979⟩

Reports4 documents

  • Thomas Bellet, Agnès Arnould, Hakim Belhaouari, Pascale Le Gall. Geometric modeling: consistency preservation using two-layered variable substitutions (extended version). [Research Report] Xlim UMR CNRS 7252; CentraleSupélec, Université Paris-Saclay. 2017. ⟨hal-01509832⟩
  • Thomas Bellet, Agnès Arnould, Pascale Le Gall. Constraint-preserving labeled graph transformations for topology-based geometric modeling. [Research Report] XLIM. 2017. ⟨hal-01476860⟩
  • Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prévosto. Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts: a detailed example of vending machine. [Research Report] Laboratoire MAS - CentraleSupelec. 2015. ⟨hal-01191890⟩
  • Imen Boudhiba, Christophe Gaston, Pascale Le Gall, Virgile Prévosto. Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts: a detailed example of vending machine. [Research Report] ECOLE CENTRALE DE PARIS; CEA-LIST. 2015. ⟨cea-01810709⟩