- 22
- 19
- 12
- 6
- 4
- 4
- 4
- 3
- 2
- 1
- 1
- 1
- 1
- 1
- 1
Pascale LE GALL
Professor in Computer Sciences
Laboratory MICS
CentraleSupélec
University of Paris-Saclay
82
Documents
Identifiants chercheurs
pascale-le-gall-
0000-0002-8955-6835
- IdRef : 081059310
Présentation
Professeur en Informatique, CentraleSupélec, CNU 27, laboratoire MICS
**Thèmes de recherche :**
Génie logiciel, Méthodes formelles, Validation et Vérification, Test de conformité, Modélisation des systèmes communicants temps-réel distribués, Modélisation géométrique à base topologique, Transformations de graphes
**Enseignenments :**
Théorie des jeux, Sémantique des langages de programmation, Logique, Automates, Bio-informatique
Publications
- 23
- 15
- 12
- 11
- 8
- 8
- 7
- 7
- 6
- 6
- 5
- 5
- 5
- 5
- 4
- 4
- 4
- 4
- 4
- 4
- 4
- 3
- 3
- 3
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 2
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 1
- 5
- 7
- 2
- 1
- 4
- 4
- 7
- 4
- 3
- 7
- 2
- 2
- 2
- 4
- 3
- 7
- 4
- 2
- 9
- 2
- 1
Efficient computation of arbitrary control dependenciesTheoretical Computer Science, 2023, 969, pp.114029. ⟨10.1016/j.tcs.2023.114029⟩
Article dans une revue
hal-04490333v1
|
|
|
|
Interaction-based offline runtime verification of distributed systemsLecture Notes in Computer Science, 2023, Fundamentals of Software Engineering, 14155, pp.88-103. ⟨10.1007/978-3-031-42441-0_7⟩
Article dans une revue
cea-04228010v1
|
|
|
Topological consistency preservation with graph transformation schemesScience of Computer Programming, 2022, 214, pp.102728. ⟨10.1016/j.scico.2021.102728⟩
Article dans une revue
hal-03380327v1
|
|
|
Preserving consistency in geometric modeling with graph transformationsMathematical Structures in Computer Science, 2022, ⟨10.1017/S0960129522000226⟩
Article dans une revue
hal-03821122v1
|
|
|
Equivalence of denotational and operational semantics for interaction languagesLecture Notes in Computer Science, 2022, Theoretical Aspects of Software Engineering, 13299, pp.113-130. ⟨10.1007/978-3-031-10363-6_8⟩
Article dans une revue
cea-04060492v1
|
|
|
Revisiting semantics of interactions for trace validity analysisLecture Notes in Computer Science, 2020, 12076, pp.482-501. ⟨10.1007/978-3-030-45234-6_24⟩
Article dans une revue
cea-04224596v1
|
Cut branches before looking for bugs: certifiably sound verification on relaxed slicesFormal Aspects of Computing, 2018, 30 (1), pp.107-131. ⟨10.1007/s00165-017-0439-x⟩
Article dans une revue
cea-01801601v1
|
|
Symbolic execution of transition systems with function summariesLecture Notes in Computer Science, 2017, 10375 LNCS, pp.41-58. ⟨10.1007/978-3-319-61467-0_3⟩
Article dans une revue
cea-01808888v1
|
|
Exhaustive test sets for algebraic specification correctnessJournal of Software Testing, Verification and Reliability, 2016, 26 (4), pp.294-317. ⟨10.1002/stvr.1598⟩
Article dans une revue
hal-01318362v1
|
|
|
|
Étude de réseaux de Thomas par validation de propriétés LTL pour Pseudomonas aeruginosaRevue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2015, 34 (5), pp.575 - 600. ⟨10.3166/TSI.34.575-600⟩
Article dans une revue
hal-01819818v1
|
|
|
Embedding of biological regulatory networks and property preservationMathematics in Computer Science, 2011, 5 (1), pp.263-288
Article dans une revue
hal-00782867v1
|
|
|
Proof-Guided Test Selection from First-Order Specifications with EqualityJournal of Automated Reasoning, 2010, 45 (4), pp.437-473
Article dans une revue
hal-00782871v1
|
Transformations de graphes pour les opérations topologiques en modélisation géométriqueRevue Electronique Francophone d'Informatique Graphique, 2010, 4 (1), http://www.irit.fr/REFIG/index.php/refig/article/view/77
Article dans une revue
hal-01137358v1
|
|
|
|
Complex software systems : Formalization and ApplicationsInternational Journal On Advances in Software, 2009, 2 (1), pp.47-62
Article dans une revue
hal-00782879v1
|
|
|
Topology-based Abstraction of Complex Biologiical Systems: Application to the Golgi ApparatusTheorie in den Biowissenschaften / Theory in Biosciences, 2008, 127 (2), pp.79-88
Article dans une revue
hal-00352003v1
|
Symbolic modeling of genetic regulatory networksJournal of Bioinformatics and Computational Biology, 2007, 5 (2B), pp.627-640
Article dans une revue
hal-00293530v1
|
|
|
|
Spécifications formelles du chanfreinageRevue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2002, 21 (8), pp.1-26
Article dans une revue
hal-00352083v1
|
|
|
Test de conformité : une approche algébriqueRevue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, 2002, 21 (9), pp.1219-1242
Article dans une revue
hal-00352131v1
|
|
|
Une approche pour inférer les expressions de calcul géométrique en modélisation à base topologique22ème Journées des Approches Formelles dans l’Assistance au Développement de Logiciels, AFADL’23., Jun 2023, Rennes, France
Communication dans un congrès
hal-04185658v1
|
|
|
An efficient VCGen-based modular verification of relational propertiesISoLA 2022 - 11th International Symposium On Leveraging Applications of Formal Methods, Verification and Validation, Oct 2022, Rhodes, Greece
Communication dans un congrès
cea-03768250v1
|
|
|
Certified verification of relational propertiesiFM 2022 : International Conference on integrated Formal Methods, Jun 2022, Lugano, Switzerland. pp.86-105, ⟨10.1007/978-3-031-07727-2_6⟩
Communication dans un congrès
cea-03714381v1
|
|
|
A small-step approach to multi-trace checking against interactionsSAC '21: The 36th ACM/SIGAPP Symposium on Applied Computing, ACM (SIGAPP), Mar 2021, Virtual Event, South Korea. pp.1815-1822, ⟨10.1145/3412841.3442054⟩
Communication dans un congrès
cea-04224612v1
|
|
|
Methodology for Specification and Verification of High-Level Requirements with MetAcslFormaliSE 2021 - 9th International Conference on Formal Methods in Software Engineering, IEEE TCSE; SIGSOFT, May 2021, Online conference, France
Communication dans un congrès
cea-03179670v1
|
|
|
MetAcsl: Specification and Verification of High-Level PropertiesTACAS 2019, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17462-0_22⟩
Communication dans un congrès
cea-02019790v1
|
|
|
Tame your annotations with MetAcsl: Specifying, Testing and Proving High-Level PropertiesInternational Conference on Tests and Proofs (TAP), Oct 2019, Porto, Portugal. ⟨10.1007/978-3-030-31157-5_11⟩
Communication dans un congrès
cea-02301892v1
|
Behavioral Models and Scenario Selection for Testing IoT Trickle-Based Lossy Multicast Networks2019 IEEE International Conference on Software Testing, Verification and Validation Workshops (ICSTW), Apr 2019, Xi'an, China. pp.168-175, ⟨10.1109/ICSTW.2019.00047⟩
Communication dans un congrès
hal-02421125v1
|
|
Fast Computation of Arbitrary Control DependenciesFASE 2018 International Conference on Fundamental Approaches to Software Engineering, Apr 2018, Thessaloniki, Greece. pp.207-224, ⟨10.1007/978-3-319-89363-1_12⟩
Communication dans un congrès
hal-02539534v1
|
|
|
|
Static and Dynamic Verification of Relational Properties on Self-Composed C CodeTests and Proofs - TAP, Jun 2018, Toulouse, France
Communication dans un congrès
cea-01835470v1
|
|
|
RPP : Preuve automatique de propriétés relationnelles par Self-CompositionApproches Formelles pour l'Assistance au Développement de Logiciels - AFADL, Jun 2018, Grenoble, France
Communication dans un congrès
cea-01835491v1
|
RPP: Automatic proof of relational properties by self-compositionTACAS 2017: Tools and Algorithms for the Construction and Analysis of Systems, Apr 2017, Uppsala, Sweden. pp.391-397, ⟨10.1007/978-3-662-54577-5_22⟩
Communication dans un congrès
cea-01808885v1
|
|
|
|
Symbolic execution of transition systems with function summaries11th International Conference on Tests & Proofs, Jul 2017, Marburg, Germany
Communication dans un congrès
cea-01810693v1
|
Geometric Modeling: Consistency Preservation Using Two-Layered Variable SubstitutionsInternational Conference on Graph Transformation ICGT 2017, Jul 2017, Marburg, Germany. pp.36-53, ⟨10.1007/978-3-319-61470-0_3⟩
Communication dans un congrès
hal-01817827v1
|
|
|
|
Constraint-Based Oracles for Timed Distributed Systems29th 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⟩
Communication dans un congrès
hal-01678964v1
|
|
|
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
Communication dans un congrès
hal-01333605v1
|
|
|
Timed-model-based Method for Security Analysis and Testing of Smart Grid Systems19th International Symposium on Real-Time Distributed Computing (ISORC) 2016, May 2016, York, United Kingdom. ⟨10.1109/isorc.2016.15⟩
Communication dans un congrès
cea-01302826v1
|
|
|
Cut branches before looking for bugs: Sound verification on relaxed slicesInternational Conference on Fundamental Approaches to Software Engineering, Apr 2016, Eindhoven, Netherlands. pp.179-196, ⟨10.1007/978-3-662-49665-7_11⟩
Communication dans un congrès
cea-01808894v1
|
|
|
Model-based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and ContractsThe 27th IFIP International Conference on Testing Software and Systems (ICTSS-2015) , Nov 2015, Sharjah and Dubai, United Arab Emirates
Communication dans un congrès
cea-01810689v1
|
Formal Analysis of the Wnt/β-catenin through Statistical Model Checking6th International Symposium, ISoLA 2014, Tiziana Margaria, Bernhard Steffen, Oct 2014, Corfu, Greece
Communication dans un congrès
hal-01110747v1
|
|
|
|
An LTL Model Checking Approach for Biological Parameter InferenceInternational Conference on Formal Engineering Methods, Nov 2014, Luxembourg, Luxembourg
Communication dans un congrès
hal-01819841v1
|
Security Weaknesses Detection by Symbolic Analysis of Scenarios2014 21st Asia-Pacific Software Engineering Conference (APSEC), Dec 2014, Jeju, South Korea. ⟨10.1109/APSEC.2014.61⟩
Communication dans un congrès
hal-01812121v1
|
|
JERBOA: A Graph Transformation Library for Topology-Based Geometric Modeling7th International Conference on Graph Transformation (ICGT 2014), Jul 2014, York, United Kingdom. ⟨10.1007/978-3-319-09108-2_18⟩
Communication dans un congrès
hal-01012851v1
|
|
Designing Sequence Diagram Models for Robustness to Attacks2014 IEEE Seventh International Conference on Software Testing, Verification and Validation Workshops (ICSTW), Mar 2014, OH, United States. ⟨10.1109/ICSTW.2014.50⟩
Communication dans un congrès
hal-01812124v1
|
|
|
|
Formal analysis of the Wnt/β-catenin pathway through statistical model checkingInternational Symposium On Leveraging Applications of Formal Methods, Verification and Validation , Oct 2014, Corfu, Greece
Communication dans un congrès
hal-01819866v1
|
|
|
An implementation relation and test framework for timed distributed systemsInternational Conference on Testing Software and Systems, Nov 2013, Istanbul, Turkey
Communication dans un congrès
cea-01810746v1
|
|
|
Off-Line Test Case Generation for Timed Symbolic Model-Based Conformance Testing24th International Conference on Testing Software and Systems (ICTSS), Nov 2012, Aalborg, Denmark. pp.119-135, ⟨10.1007/978-3-642-34691-0_10⟩
Communication dans un congrès
hal-01482398v1
|
|
|
JERBOA : un modeleur géométrique à base de règlesApproches Formelles dans l'Assistance au Développement de Logiciels (AFADL), Jan 2012, Grenoble, France
Communication dans un congrès
hal-00936743v1
|
Rule-based transformations for geometric modeling6th International Workshop on Computing with Terms and Graphs (TERMGRAPH 2011), Part of ETAPS 2011, Apr 2011, Saarbrücken, Germany. 20p
Communication dans un congrès
hal-00865432v1
|
|
Testing web service orchestrators in context : a symbolic approachSEFM 2010 : 8th IEEE International Conference on Software Engineering and Formal Methods, Sep 2010, Pisa, Italy. pp.257 - 267, ⟨10.1109/SEFM.2010.30⟩
Communication dans un congrès
hal-01306744v1
|
|
Designing a Topological Modeler Kernel: A Rule-Based ApproachShape Modeling International (SMI'10), Jun 2010, Aix-en-Provence, France
Communication dans un congrès
hal-00488171v1
|
|
Transformations de graphes pour les opérations topologiques en modélisation géométrique22es Journées de l'Association Francophone d'Informatique Graphique, chapitre français d'Eurographics (AFIG 2009), Nov 2009, Arles, France
Communication dans un congrès
hal-00488533v1
|
|
Observability and controllability issues in conformance testing of Web service compositionsTESTCOM/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⟩
Communication dans un congrès
hal-01360755v1
|
|
Generation of All-Paths Unit Test with Function CallsFirst 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⟩
Communication dans un congrès
hal-01810199v1
|
|
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⟩
Communication dans un congrès
hal-00341176v1
|
|
Testing of Software and Communicating Systems20th 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⟩
Communication dans un congrès
hal-00289229v1
|
|
|
|
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⟩
Communication dans un congrès
hal-00812184v1
|
Test selection criteria for quantifier-free first-order specifications2nd IPM International Symposium on Fundamentals of Software Engineering (FSEN 2007), Apr 2007, Tehran, Iran. pp.144-159, ⟨10.1007/978-3-540-75698-9_10⟩
Communication dans un congrès
hal-00353787v1
|
|
|
|
Topology-based Geometric Modelling for Biological Cellular ProcessesInternational Conference on Language and Automata Theory and Applications, Mar 2007, Tarragone, Spain. pp.497-508
Communication dans un congrès
hal-00348152v1
|
|
|
Exploring Topological Modelling to Discriminate Models of Golgi Apparatus DynamicsEuropean Conference on Complex Systems (ECCS), Oct 2007, Dresde, Germany
Communication dans un congrès
hal-00348154v1
|
|
|
Feature specification and static analysis for interaction resolution14th International Symposium on Formal Methods (FM 2006), Aug 2006, Hamilton, Canada. pp.364--379, ⟨10.1007/11813040_25⟩
Communication dans un congrès
hal-00341977v1
|
Symbolic execution techniques for test purpose definitionProceedings of the 18th international conference on Testing of Communicating Systems (TestCom), 2006, United States. pp.1--18
Communication dans un congrès
hal-00342082v1
|
|
Automatic generation of symbolic test purposesProceedings of the second MoDeVa (Model Design and Validation) workshop, 2005, Jamaica. pp.n.a
Communication dans un congrès
hal-00342173v1
|
|
Evaluation symbolique appliquée à l'étude de réseaux de régulation génétiqueJournée Thématique <>, 2005, France. pp.n.a
Communication dans un congrès
hal-00342150v1
|
|
|
|
A Temporal Logic for Input Output Symbolic Transition Systems12th Asia-Pacific Software Engineering Conference (APSEC'05), Dec 2005, Taipei, Taiwan. pp.43--50, ⟨10.1109/APSEC.2005.19⟩
Communication dans un congrès
hal-00341980v1
|
An Automatic Off-Line Feature Interaction Detection Method by Static Analysis of SpecificationsProceedings of the 8th International Conference on Feature Interactions in Telecommunications and Software Systems (FIW'05), 2005, United Kingdom. pp.131--146
Communication dans un congrès
hal-00342087v1
|
|
|
|
Testing from algebraic specifications: test data set selection by unfolding axioms5th International Workshop on Formal Approaches to Testing of Software (FATES 2005), 2005, Edinburgh, United Kingdom. pp.203--217, ⟨10.1007/11759744_14⟩
Communication dans un congrès
hal-00341964v1
|
Testing from Abstract Data Type SpecificationsTraining And Research On Testing (TAROT) Summer School, 2005, France. pp.n.a
Communication dans un congrès
hal-00342088v1
|
|
Spécifications formelles du chanfreinageAFADL2001, Jan 2001, X, France
Communication dans un congrès
hal-01124624v1
|
|
|
Inference of geometric modeling operationsPoster de conférence hal-04068329v1 |
|
|
A first step towards the inference of geological topological operationsEurographics 2022, Apr 2022, Reims, France. 2022, ⟨10.2312/egp.20221005⟩
Poster de conférence
hal-03664618v1
|
Testing Software and SystemsSpringer International Publishing, LNCS-11812, 2019, Lecture Notes in Computer Science, 978-3-030-31279-4. ⟨10.1007/978-3-030-31280-0⟩
Ouvrages
hal-02526347v1
|
|
|
Transformations de graphes décorésLaurent Fuchs (éd.). Informatique Mathématique Une photographie en 2023, CNRS, Chapitre 4, pp. 133 -- 178, 2023, CNRS Alpha, 978-2-271-14930-5
Chapitre d'ouvrage
hal-04187816v1
|
|
|
Model-based Testing from Input Output Symbolic Transition Systems Enriched by Program Calls and ContractsTesting Software and Systems , 9447), pp.35-51, 2014, Lecture Notes in Computer Science, ⟨10.1007/978-3-319-25945-1_3⟩
Chapitre d'ouvrage
hal-01470156v1
|
Symbolic Execution-Based Techniques for Conformance TestingModel‐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⟩
Chapitre d'ouvrage
cea-01818541v1
|
|
|
|
Testing data types implementations from algebraic specificationsR. 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⟩
Chapitre d'ouvrage
hal-00270574v1
|
Toward a computer-aided methodology for topology-based simulation of the Golgi apparatusProc. of the Lille Spring school on Modelling and simulation of biological processes in the context of genomics, EDP SCIENCES, pp.89--104, 2008
Chapitre d'ouvrage
hal-00353755v1
|
EditorialAutre publication scientifique cea-04129929v1 |
|
Feature specification: a logic-independent approach2005
Autre publication scientifique
hal-00341979v1
|
|
Generating test case from symbolic transition systems based on constrained unfolding2005
Autre publication scientifique
hal-00342083v1
|
|
A temporal logic for input output symbolic transition systems2005
Autre publication scientifique
hal-00341981v1
|
|
|
Geometric modeling: consistency preservation using two-layered variable substitutions (extended version)[Research Report] Xlim UMR CNRS 7252; CentraleSupélec, Université Paris-Saclay. 2017
Rapport
hal-01509832v1
|
|
|
Constraint-preserving labeled graph transformations for topology-based geometric modeling[Research Report] XLIM. 2017
Rapport
hal-01476860v1
|
|
|
Input Output Symbolic Transition Systems Enriched by Program Calls and Contracts: a detailed example of vending machine[Research Report] Laboratoire MAS - CentraleSupelec. 2015
Rapport
hal-01191890v1
|