A. Sy, 102) (30) 1.46 (30) 0.34 (100) 39, pp.37300-37301, 0200.

I. Dans-la-partie, Ces techniques utilisent des algorithmes polynomiaux ? à condition d'utiliser les algorithmes récents pour tester l'inclusion des langages de deux automates, comme dans [DR10, ACH + 10, BP12] ?, et ne sont pas liées au spécificités d'un domaine en particulier (elles sont applicables à tous types de problèmes réguliers) Nos propositions ? contrairement à [BJNT00, BHV04] dont elles sont inspirées ? n'exigent pas de minimiser/déterminiser l'automate obtenu à chaque étape du model-checking régulier. Nous avons publié ces travaux dans [DHK13a] Comme une direction possible de ces travaux, nous pouvons envisager de les adapter aux langages d'arbres, comme l'ont fait par exemple les auteurs de [BJNT00, BHV04] ; car après avoir défini une méthode de vérification qui fonctionne sur les mots, vient naturellement l'envie de la confronter à un modèle plus puissant comme les arbres. Mais avant cela, nous n'avons pas épuisé les idées d'améliorations de notre méthode sur les mots... Nous pensons que notre approche de raffinement doit pouvoir être améliorée, sur la précision des approximations comme sur le temps de calcul. Par exemple, pour la technique dont la fonction d'approximation est l'automate C, nous raffinons actuellement en dupliquant simplement l'état p de C qui correspond à la classe d'équivalence des états que l'on ne souhaite plus fusionner Au lieu de ça, nous pourrions essayer de dupliquer l'ensemble de l'automate C, afin de séparer également les états de C qui suivent l'état p ? nous avons nommé cette idée raffinement par couleur. Une autre idée que nous n'avons pas eu le temps d'approfondir est d'éviter de fusionner entre eux des états qui étaient déjà présents dans l'automate précédent, afin que l'automate A i ressemble davantage à l'automate A i?1, nous avons défini et présenté deux nouvelles techniques d'approximation pour le model-checking régulier (cf. problème 3.3) (cf. [BFL04]) ou encore les systèmes à pile, p.40

I. Dans-la-partie, Combiner génération aléatoire et critère de couverture, à partir d'une grammaire algébrique ou d'un automate à pile), nous avons présenté et développé deux méthodes automatiques qui permettent d'exploiter à la fois critère de couverture et test aléatoire. La première permet de générer des tests à partir d'une grammaire

. A. Bibliographie-[-ach-+-10-]-p, Y. Abdulla, L. Chen, R. Holík, T. Mayr et al., When simulation meets antichains, pp.158-174

R. H. Agrawal, R. Demillo, W. Hathaway, W. Hsu, E. Hsu et al., Design of mutant operators for the c programming language, 1989.

]. P. Ajmd02, B. Abdulla, P. Jonsson, and J. Mahata, Regular tree model checking, Proceedings of the 14th international conference on Computer Aided Verification, CAV'02, pp.452-466, 2002.

P. A. Abdulla, B. Jonsson, M. Nilsson, and J. , Algorithmic Improvements in Regular Model Checking, Hunt and Somenzi [HS03], pp.236-248
DOI : 10.1007/978-3-540-45069-6_25

R. Alur and P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing , STOC '04, pp.202-211, 2004.
DOI : 10.1145/1007352.1007390
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.116.3757

P. Ammann and J. Offutt, Introduction to Software Testing, 2008.
DOI : 10.1017/CBO9780511809163

T. L. Alves and J. Visser, A Case Study in Grammar Engineering, LNCS, vol.12, issue.4, pp.285-304, 2008.
DOI : 10.1007/3-540-45937-5_12

Y. Boichut, R. Courbis, P. Héam, and O. Kouchnarenko, Finer Is Better: Abstraction Refinement for Rewriting Approximations, Proceedings of the 19th international conference on Rewriting Techniques and Applications, RTA'08, pp.48-62, 2008.
DOI : 10.1007/978-3-540-70590-1_4
URL : https://hal.archives-ouvertes.fr/hal-00563422

A. Bouajjani, J. Esparza, A. Finkel, O. Maler, P. Rossmanith et al., An efficient automata approach to some problems on context-free grammars, Information Processing Letters, vol.74, issue.5-6, pp.5-6221, 2000.
DOI : 10.1016/S0020-0190(00)00055-7

B. Beizer, Black Box Testing: Techniques for Functional Testing of Software and Systems, IEEE Software, vol.13, issue.5, 1995.
DOI : 10.1109/MS.1996.536464

A. Bauer and Y. Falcone, Decentralised LTL monitoring, LNCS, vol.7436, pp.85-100, 2012.
DOI : 10.1007/978-3-642-32759-9_10
URL : https://hal.archives-ouvertes.fr/hal-00857286

S. Bardin, A. Finkel, and J. Leroux, FASTer Acceleration of Counter Automata in Practice, Proceedings of the 10th international conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS'04, pp.576-590, 2004.
DOI : 10.1007/978-3-540-24730-2_42

S. Bardin, A. Finkel, J. Leroux, and L. Petrucci, FAST: Fast Acceleration of Symbolic Transition Systems, Hunt and Somenzi [HS03], pp.118-121
DOI : 10.1007/978-3-540-45069-6_12
URL : https://hal.archives-ouvertes.fr/hal-00084185

A. Bouajjani, P. Habermehl, and T. Vojnar, Abstract Regular Model Checking, Proceedings of the 16th international conference on Computer Aided Verification, pp.378-379, 2004.
DOI : 10.1007/978-3-540-27813-9_29
URL : https://hal.archives-ouvertes.fr/hal-00159512

A. Bouajjani, B. Jonsson, M. Nilsson, and T. Touili, Regular Model Checking, pp.403-418
DOI : 10.1007/10722167_31
URL : https://hal.archives-ouvertes.fr/hal-00159512

C. Baier, J. P. Katoen, and I. Ebrary, Principles of model checking, 2008.

B. Boigelot, A. Legay, and P. Wolper, Iterating Transducers in the Large, Hunt and Somenzi [HS03], pp.223-235
DOI : 10.1007/978-3-540-45069-6_24

B. Boigelot, Domain-specific regular acceleration, International Journal on Software Tools for Technology Transfer, vol.10, issue.3, pp.193-206, 2012.
DOI : 10.1007/s10009-011-0206-x
URL : http://orbi.ulg.ac.be/jspui/handle/2268/135057

F. Bonchi and D. Pous, Checking NFA equivalence with bisimulations up to congruence, p.13, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00639716

S. Basu, D. Saha, Y. Lin, and S. A. Smolka, Generation of All Counter-Examples for Push-Down Systems, Proceedings of the 23rd IFIP WG 6.1 international conference , FORTE'03, pp.79-94, 2003.
DOI : 10.1007/3-540-58950-3_371

A. Bouajjani and T. Touili, Widening techniques for regular tree model checking, International Journal on Software Tools for Technology Transfer, vol.962, issue.1, pp.1-21, 2011.
DOI : 10.1007/s10009-011-0208-8

E. M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, Counterexample-guided abstraction refinement, Emerson and Sistla [ES00], pp.154-169

C. Campbell, W. Grieskamp, L. Nachmanson, W. Schulte, N. Tillmann et al., Testing Concurrent Object-Oriented Systems with Spec Explorer, FM'05, pp.542-547, 2005.
DOI : 10.1007/11526841_38

E. M. Clarke, O. Grumberg, and D. Peled, Model Checking, 2000.

D. Coppit and J. Lian, yagg, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering , ASE '05, pp.356-359
DOI : 10.1145/1101908.1101969

R. Clark, Querying streaming xml using visibly pushdown automata, 2008.

B. Daniel, D. Dig, K. Garcia, and D. Marinov, Automated testing of refactoring engines, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering , ESEC-FSE '07, 2007.
DOI : 10.1145/1287624.1287651

A. Denise, I. Dutour, and P. Zimmermann, Cs : a mupad package for counting and randomly generating combinatorial structures, Proceedings of the 10-th international conference on Formal Power Series and Algebraic Combinatorics, FPSAC'98, pp.195-204, 1998.
URL : https://hal.archives-ouvertes.fr/inria-00107518

S. Gaudel, R. Gouraud, J. Lassaigne, S. Oudinet, and . Peyronnet, Coverage-biased random exploration of large models and application to testing, International Journal on Software Tools for Technology Transfer, STTT, issue.1, pp.1473-93, 2012.
URL : https://hal.archives-ouvertes.fr/inria-00560621

]. A. Dhk13a, P. Dreyfus, O. Héam, and . Kouchnarenko, Enhancing approximations for regular reachability analysis, Implementation and Application of Automata, pp.331-339, 2013.

]. A. Dhk13b, P. Dreyfus, O. Héam, and . Kouchnarenko, Random grammar-based testing for covering all non-terminals, Software Testing, Verification and Validation Workshops (ICSTW), 2013 IEEE Sixth International Conference on, pp.210-215, 2013.

P. [. Dreyfus, O. Héam, C. Kouchnarenko, and . Masson, A random testing approach using pushdown automata. Software Testing, Verification and Reliability, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01088712

E. W. Dijkstra, Algol 60 translation : An Algol 60 translator for the x1 and Making a translator for Algol 60, Mathematisch Centrum, 1961.

F. Dadeau, J. Levrey, and P. Héam, On the Use of Uniform Random Generation of Automata for Testing, Electronic Notes in Theoretical Computer Science, vol.253, issue.2, pp.37-51, 2009.
DOI : 10.1016/j.entcs.2009.09.050
URL : https://hal.archives-ouvertes.fr/inria-00429236

D. Dams, Y. Lakhnech, and M. Steffen, Iterating transducers, Proceedings of the 13th international conference on Computer Aided Verification, CAV'01, pp.286-297, 2001.
DOI : 10.1007/3-540-44585-4_27

D. Dams, Y. Lakhnech, and M. Steffen, Iterating transducers, Journal of Logic and Algebraic Programming, vol.52, pp.109-127, 2002.
DOI : 10.1007/3-540-44585-4_27

J. W. Duran and S. Ntafos, A report on random testing, Proceedings of the 5th international conference on Software engineering, ICSE'81, pp.179-183, 1981.

L. Doyen and J. Raskin, Antichain Algorithms for Finite Automata, pp.2-22
DOI : 10.1007/978-3-642-12002-2_2

A. Denise and P. Zimmermann, Uniform random generation of decomposable structures using floating-point arithmetic, Theoretical Computer Science, vol.218, issue.2, pp.233-248, 1999.
DOI : 10.1016/S0304-3975(98)00323-5
URL : https://hal.archives-ouvertes.fr/inria-00073447

I. Enderlin, F. Dadeau, A. Giorgetti, and F. Bouquet, Grammar-Based Testing Using Realistic Domains in PHP, 2012 IEEE Fifth International Conference on Software Testing, Verification and Validation, pp.509-518, 2012.
DOI : 10.1109/ICST.2012.136
URL : https://hal.archives-ouvertes.fr/hal-00931662

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon, Efficient Algorithms for Model Checking Pushdown Systems, Proceedings of the 12th international conference on Computer Aided Verification, CAV'00, pp.232-247, 2000.
DOI : 10.1007/10722167_20

I. Enderlin, Hoa project, a set of php libraries

F. Fioravanti, A. Pettorossi, M. Proietti, and V. Senni, Program specialization for verifying infinite state systems : An experimental evaluation. Logic-Based Program Synthesis and Transformation, pp.164-183, 2011.

P. Flajolet and R. Sedgewick, Analytic Combinatorics, 2008.
DOI : 10.1017/CBO9780511801655
URL : https://hal.archives-ouvertes.fr/inria-00072739

P. Flajolet, P. Zimmermann, and B. Van-cutsem, A calculus for the random generation of labelled combinatorial structures, Theoretical Computer Science, vol.132, issue.1-2, pp.1-35, 1994.
DOI : 10.1016/0304-3975(94)90226-7
URL : https://hal.archives-ouvertes.fr/hal-00917729

M. Gaudel, Le test de logiciel : pourquoi et comment. 1024 ? Bulletin de la société informatique de France, Available, pp.1024-1027, 2014.

A. Gotlieb, B. Botella, and M. Rueher, Automatic test data generation using constraint solving techniques, Proceedings of the ACM SIGSOFT International Symposium on Software Testing and Analysis, ISSTA'98, pp.53-62, 1998.

A. Gotlieb, T. Denmat, and B. Botella, Constraint-based test data generation in the presence of stack-directed pointers, Proceedings of the 20th IEEE/ACM international Conference on Automated software engineering , ASE '05, pp.313-316
DOI : 10.1145/1101908.1101958

A. Cano-gómez, G. Guaiana, and J. Pin, When does partial commutative closure preserve regularity ?, Proceedings of the 35th International Colloquium on Automata, Languages and Programming, ICALP'08, pp.209-220, 2008.

A. Groce and R. Joshi, Random testing and model checking, Proceedings of the 2008 international workshop on dynamic analysis held in conjunction with the ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA 2008), WODA '08, pp.22-28, 2008.
DOI : 10.1145/1401827.1401833

P. Godefroid, A. Kiezun, and M. Y. Levin, Grammar-based whitebox fuzzing, PLDI, pp.206-215, 2008.
DOI : 10.1145/1379022.1375607
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.165.770

P. Godefroid, N. Klarlund, and K. Sen, DART : directed automated random testing, PLDI'05 : Proceedings of the 2005 ACM SIGPLAN conference on Programming language design and implementation, pp.213-223, 2005.

C. Grandpierre, Stratégies de génération automatique de tests à partir de modèles comportementaux UML/OCL, 2008.

R. Hamlet, Random Testing, Encyclopedia of Software Engineering, pp.970-978, 1994.
DOI : 10.1002/0471028959.sof268

T. J. Hickey and J. Cohen, Uniform Random Generation of Strings in a Context-Free Language, SIAM Journal on Computing, vol.12, issue.4, pp.645-655, 1983.
DOI : 10.1137/0212044

P. Héam and C. Nicaud, Seed: An Easy-to-Use Random Generator of Recursive Data Structures for Testing, 2011 Fourth IEEE International Conference on Software Testing, Verification and Validation, pp.60-69, 2011.
DOI : 10.1109/ICST.2011.31

M. Hague and C. Ong, Analysing Mu-Calculus Properties of Pushdown Systems, Proceeding of the 17th international SPIN workshop, pp.187-192, 2010.
DOI : 10.1007/978-3-642-16164-3_14

C. Jard and T. Jéron, TGV: theory, principles and algorithms, International Journal on Software Tools for Technology Transfer, vol.17, issue.4, 2004.
DOI : 10.1007/s10009-004-0153-x

B. Jonsson and M. Nilsson, Transitive Closures of Regular Relations for Verifying Infinite-State Systems, TACAS, pp.220-235, 2000.
DOI : 10.1007/3-540-46419-0_16

. Kmm-+-97-]-y, O. Kesten, M. Maler, A. Marcus, E. Pnueli et al., Symbolic model checking with rich assertional languages, Proceedings of the 9th PARTIE IV. Conclusions et perspectives -BIBLIOGRAPHIE 123

A. Legay, Extrapolating (omega-)regular model checking, International Journal on Software Tools for Technology Transfer, vol.3, issue.4, pp.119-143, 2012.
DOI : 10.1007/s10009-011-0209-7

T. , L. Gall, B. Jeannet, and T. Jéron, Verification of communication protocols using abstract interpretation of fifo queues, Algebraic Methodology and Software Technology, pp.204-219, 2006.

R. Lämmel and W. Schulte, Controllable Combinatorial Coverage in Grammar-Based Testing, LNCS, vol.3964, pp.19-38, 2006.
DOI : 10.1007/11754008_2

D. Lee and M. Yannakakis, Principles and methods of testing finite state machines-a survey, Proceedings of the IEEE, pp.1090-1123, 1996.
DOI : 10.1109/5.533956

P. M. Maurer, The design and implementation of a grammar-based data generator, Software: Practice and Experience, vol.5, issue.3, pp.223-244, 1992.
DOI : 10.1002/spe.4380220303

K. Eikland, M. Berkelaar, and P. Notebaert, lp_solve : a mixed interger linear program, 2004.

B. Mckenzie, Generating string at random from a context-free grammar, 1997.

R. Majumdar and R. Xu, Directed test generation using symbolic grammars, pp.134-143, 2007.
DOI : 10.1145/1321631.1321653
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.133.4430

C. Oriat, Jartege: A Tool for Random Generation of Unit Tests for Java Classes, LNCS, vol.3712, pp.242-256, 2005.
DOI : 10.1007/11558569_18
URL : https://hal.archives-ouvertes.fr/hal-00003466

A. J. Offutt, Y. Xiong, and S. Liu, Criteria for generating specification-based tests, Proceedings Fifth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS'99) (Cat. No.PR00434), pp.119-129, 1999.
DOI : 10.1109/ICECCS.1999.802856

Y. Ponty, M. Termier, and A. Denise, GenRGenS: software for generating random genomic sequences and structures, Bioinformatics, vol.22, issue.12, pp.1534-1535, 2006.
DOI : 10.1093/bioinformatics/btl113
URL : https://hal.archives-ouvertes.fr/inria-00548871

P. Purdom, A sentence generator for testing parsers, BIT, vol.9, issue.1, pp.366-375, 1972.
DOI : 10.1007/BF01932308

S. Schwoon, Model-Checking Pushdown Systems, 2002.

M. Sipser, Introduction to the Theory of Computation, ACM SIGACT News, vol.27, issue.1, pp.27-29, 1996.
DOI : 10.1145/230514.571645

F. Song and T. Touili, Efficient CTL model-checking for pushdown systems, CONCUR'11 : Proceedings of the 22nd International Conference on Concurrency Theory, pp.434-449, 2011.

F. Song and T. Touili, PuMoC: a CTL model-checker for sequential programs, Proceedings of the 27th IEEE/ACM International Conference on Automated Software Engineering, ASE 2012, pp.346-349, 2012.
DOI : 10.1145/2351676.2351743

P. Thévenod-fosse, Software Validation by Means of Statistical Testing: Retrospect and Future Direction, International Working Con-ference on Dependable Computing for Criti-cal Applications, 1989.
DOI : 10.1007/978-3-7091-9123-1_2

T. Touili, Regular Model Checking using Widening Techniques, VEPAS, pp.342-356, 2001.
DOI : 10.1016/S1571-0661(04)00187-2
URL : https://hal.archives-ouvertes.fr/hal-00161116

J. Tretmans, Model based testing -property checking for real In Keynote address at the international workshop for Construction and Analysis of Safe Secure, and Interoperable Smart devices, CASSIS'04 Available http, 2004.

M. Utting, A. Pretschner, and B. Legeard, A taxonomy of model-based testing approaches . Software Testing, Verification and Reliability, pp.297-312, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00940611

P. Wolper and B. Boigelot, Verifying systems with infinite but regular state spaces, Proceedings of the 10th international conference on Computer Aided Verification, CAV'98, pp.88-97, 1998.
DOI : 10.1007/BFb0028736

B. [. Williams, P. Marre, M. Mouy, and . Roger, PathCrawler: Automatic Generation of Path Tests by Combining Static and Dynamic Analysis, LNCS, vol.3463, pp.281-292, 2005.
DOI : 10.1007/11408901_21

Z. Xu, L. Zheng, and H. Chen, A Toolkit for Generating Sentences from Context-Free Grammars, 2010 8th IEEE International Conference on Software Engineering and Formal Methods, pp.118-122, 2010.
DOI : 10.1109/SEFM.2010.21

F. Yu, T. Bultan, and O. Ibarra, Relational string verification using multi-track automata, IJFCS, vol.22, pp.290-299, 2011.

L. Zheng and D. Wu, A Sentence Generation Algorithm for Testing Grammars, 2009 33rd Annual IEEE International Computer Software and Applications Conference
DOI : 10.1109/COMPSAC.2009.193

. Dans-la-partie-vérification, deux nouvelles techniques d'approximation sont définies, dans le but de fournir des (semi-)algorithmes efficaces Des surapproximations de l'ensemble des états accessibles sont calculées, avec l'objectif d'assurer la terminaison de l'exploration de l'espace d'états. Les états accessibles (ou des sur-approximations de cet ensemble d'états) sont représentés par des langages réguliers, ou automates d'états finis. La première technique consiste à surapproximer l'ensemble des états atteignables en fusionnant des états des automates, en fonction de critères syntaxiques simples, ou d'une combinaison de ces critères. La seconde technique d'approximation consiste aussi à fusionner des états des automates, mais à l'aide de transducteurs. De plus, pour cette seconde technique