Publications

A more complete list can be found at http://lifc.univ-fcomte.fr/~publis/papers/Author/DADEAU-F.html

Proceedings

  • Frédéric Dadeau and Pascale Le Gall, editors. AFADL'15, Actes des 14èmes journèes sur les Approches Formelles dans l'Assistance au Developpement de Logiciels, Bordeaux, France, May 2015.

Book chapter

  • Frédéric Dadeau, Fabien Peureux, Bruno Legeard, Régis Tissot, Jacques Julliand, Pierre-Alain Masson, and Fabrice Bouquet. Test Generation using Symbolic Animation of Models. In Model-Based Testing for Embedded Systems, Series on Computational Analysis, Synthesis, and Design of Dynamic Systems, pages 195--218. CRC Press, 2011.

Journals

  • Safouan Taha, Jacques Julliand, Frédéric Dadeau, Kalou Cabrera Castillos, and Bilal Kanso. A Compositional Automata-based Semantics and Preserving Transformation Rules for Testing Property Patterns. FAC, Formal Aspects of Computing, 27(4):641--664, 2015. Note: Revised and extended version of a paper from the iFM'13 conference.

  • Frédéric Dadeau, Pierre-Cyrille Héam, Rafik Kheddam, Ghazi Maatoug, and Michael Rusinowitch. Model-Based Mutation Testing from Security Protocols in HLPSL. Software Testing, Verification and Reliability. Special issue on Mutation Testing, 25(5-7):684--711, 2015.

  • Frédéric Dadeau, Kalou Cabrera Castillos, and Régis Tissot. Scenario-Based Testing using Symbolic Animation of B Models. Software Testing, Verification and Reliability, 22(6):407--434, September 2012.

  • Kalou Cabrera Castillos, Frédéric Dadeau, and Jacques Julliand. Scenario-Based Testing from UML/OCL Behavioral Models -- Application to POSIX Compliance. STTT, International Journal on Software Tools for Technology Transfer, 13(5):431--448, 2011. Note: Special Issue on Verified Software: Tools, Theory and Experiments (VSTTE'09).

  • Frédéric Dadeau, Amal Haddad, and Thierry. Moutet. Test fonctionnel de conformité vis-à-vis d'une politique de contrôle d'accès. TSI, Technique et Science Informatiques, 28(4):533--563, April 2009.

  • Vincent Pretre, Adrien de Kermadec, Fabrice Bouquet, Christophe Lang and Frédéric Dadeau. Automated UML models merging for web services testing. Int. Journal on Web and Grid Services, 5(2):107--129, 2009.

International conferences and workshops

  • Alexandre Vernotte, Frédéric Dadeau, Franck Lebeau, Bruno Legeard, Fabien Peureux and François Piat. Efficient Detection of Multi-step Cross-Site Scripting Vulnerabilities. ICISS 2014, 10th International Conference on Information Systems Security. Hyderabad, India. December 2014.

  • Kalou Cabrera Castillos, Frédéric Dadeau, and Jacques Julliand. Coverage Criteria for Model-Based Testing using Property Patterns. In A. Petrenko and H. Schlingloff, editors, MBT 2014, 9th International Workshop on Model-Based Testing (co-located with ETAPS 2014). Grenoble, France. April 2014.

  • Ghazi Maatoug, Frédéric Dadeau, and Michael Rusinowitch. Model-Based Vulnerability Testing of Payment Protocol Implementations. HotSpot'2014, 2nd Workshop on Hot Issues in Security Principles and Trust. Grenoble, France. April 2014.

  • Kalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand, Bilal Kanso, and Safouan Taha. A Compositional Automata-based Semantics for Property Patterns. In E.B. Johnsen and L. Petre, editors, iFM 2013, 10th International Conference on integrated Formal Methods, volume 7940 of LNCS, Turku, Finland, pages 316--330, June 2013. Springer.

  • Frédéric Dadeau, Kalou Cabrera Castillos, Yves Ledru, Taha Triki, German Vega, Julien Botella, and Safouan Taha. Test Generation and Evaluation from High-Level Properties for Common Criteria Evaluations - The TASCCC Testing Tool. In B. Baudry and A. Orso, editors, ICST 2013, 6th Int. Conf. on Software Testing, Verification and Validation, Testing Tool track, Luxemburg, Luxemburg, pages 431--438, March 2013. IEEE Computer Society Press.

  • Ivan Enderlin, Frédéric Dadeau, Alain Giorgetti, and Fabrice Bouquet. Grammar-Based Testing using Realistic Domains in PHP. In A-MOST 2012, 8th Workshop on Advances in Model Based Testing, joint to the ICST'12 IEEE Int. Conf. on Software Testing, Verification and Validation, Los Alamitos, CA, United States, pages 509--518, April 2012. IEEE Computer Society.

  • Taha Triki, Yves Ledru, Lydie du Bousquet, Frédéric Dadeau, and Julien Botella. Model-Based Filtering of Combinatorial Test Suites. In J. de Lara and A. Zisman, editors, FASE'2012, 15th Int. Conf. on Fundamental Approaches to Software Engineering, volume 7212 of LNCS, Tallinn, Estonia, pages 439--454, March 2012.

  • Kalou Cabrera Castillos, Frédéric Dadeau, Jacques Julliand, and Safouan Taha. Measuring Test Properties Coverage for evaluating UML/OCL Model-Based Tests. In B. Wolff and F. Zaidi, editors, ICTSS'11, 23-th IFIP Int. Conf. on Testing Software and Systems, volume 7019 of LNCS, Paris, France, pages 32--47, November 2011. Springer.

  • Frédéric Dadeau, Pierre-Cyrille Héam, and Rafik Kheddam. Mutation-Based Test Generation from Security Protocols in HLPSL. In M. Harman and B. Korel, editors, ICST 2011, 4th Int. Conf. on Software Testing, Verification and Validation, Berlin, Germany, pages 240--248, March 2011. IEEE Computer Society Press.

  • Frédéric Dadeau and Fabien Peureux. Grey-box Testing and Verification of Java/JML. In CSTVA'11, 3rd Int. Workshop on Constraint in Software Testing Verification and Analysis - co-located with ICST'2011, Berlin, Germany, pages 298--303, March 2011. IEEE Computer Society Press.

  • Ivan Enderlin, Frédéric Dadeau, Alain Giorgetti, and Abdallah Ben Othman. Praspel: A Specification Language for Contract-Based Testing in PHP. In B. Wolff and F. Zaidi, editors, ICTSS'11, 23-th IFIP Int. Conf. on Testing Software and Systems, volume 7019 of LNCS, Paris, France, pages 64--79, November 2011. Springer.

  • Elizabeta Fourneret, Fabrice Bouquet, Frédéric Dadeau, and Stéphane Debricon. Selective Test Generation Method for Evolving Critical Systems. In REGRESSION'11, 1st Int. Workshop on Regression Testing - co-located with ICST'2011, Berlin, Germany, pages 125--134, March 2011. IEEE Computer Society Press.

  • Pierre-Christophe Bué, Frédéric Dadeau, and Pierre-Cyrille Héam. Model-Based Testing using Symbolic Animation and Machine Learning. In CSTVA'10, 2nd Int. Workshop on Constraints in Software Testing Verification and Analysis - co-located with ICST'2010, Paris, France, pages 355--360, April 2010. IEEE Computer Society Press.

  • Pierre-Christophe Bué, Frédéric Dadeau, Adrien de Kermadec, and Fabrice Bouquet. Building a Test-ready Abstraction of a Behavioral Model using CLP. In G. Fraser and A. Gargantini, editors, TAP'10, 4-th Int. Conf. on Tests and Proofs, volume 6143 of LNCS, Malaga, Spain, pages 167--182, July 2010.

  • Adrien de Kermadec, Frédéric Dadeau, and Fabrice Bouquet. Assessing the Quality of B Models. In SEFM'2010, 8th IEEE Int. Conf. on Software Engineering and Formal Methods, Pisa, Italy, pages 83--90, September 2010. IEEE Computer Society Press.

  • Frédéric Dadeau, Pierre-Cyrille Héam, and Jocelyn Levrey. On the Use of Uniform Random Generation of Automata for Testing. In B. Finkbeiner, Y. Gurevich, and A.K. Petrenko, editors, MBT'09 proceedings, volume 253-2 of ENTCS, Electronic Notes in Theoretical Computer Science, York, United Kingdom, pages 37--51, March 2009.

  • Frédéric Dadeau and Régis Tissot. jSynoPSys -- A Scenario-Based Testing Tool based on the Symbolic Animation of B Machines. In B. Finkbeiner, Y. Gurevich, and A.K. Petrenko, editors, MBT'09 proceedings, volume 253-2 of ENTCS, Electronic Notes in Theoretical Computer Science, York, United Kingdom, pages 117--132, October 2009.

  • Frédéric Dadeau, Jacques Julliand, and Régis Tissot. Leirios Test Generator: from Research to Teaching, through Industry. In C. Attiogbé and E. Habrias, editors, Int. Workshop on the B Method: from Research to Teaching, Nantes, France, pages 1--16, June 2008. APCB.

  • Frédéric Dadeau, Julien Lamboley, Thierry Moutet, and Marie-Laure Potet. A Verifiable Conformance Relationship between Smart Card Applets and B Models. In E. Borger, J. Bowen, and M. Butler, editors, ABZ'2008, International Conference on ASM, B and Z, volume 5238 of LNCS, London, United Kingdom, pages 237--250, September 2008. Springer.

  • Frédéric Dadeau, Marie-Laure Potet, and Régis Tissot. A B Formal Framework for Security Developments in the Domain of Smart Card Applications. In S. Jajodia and P. Samarati, editors, SEC'2008, 23rd int. Information Security Conference, volume 278 of IFIP, Milano, Italy, pages 141--155, September 2008. Springer.

  • Frédéric Dadeau and Régis Tissot. Teaching Model-Based Testing with Leirios Test Generator. In Z. Istenes, editor, FORMED'08, Int. Workshop on Formal Methods in Computer Science Education, co-located with ETAPS'2008), Budapest, Hungary, pages 129--138, March 2008.

  • Frédéric Dadeau, Adrien de Kermadec, and Régis Tissot. Combining Scenario and Model-Based Testing to ensure POSIX Compliance. In E. Borger, J. Bowen, and M. Butler, editors, ABZ'2008, Int. Conf. on ASM, B and Z, volume 5238 of LNCS, London, United Kingdom, pages 153--166, September 2008. Springer.

  • Fabrice Bouquet, Jean-François Couchot, Frédéric Dadeau, and Alain Giorgetti. Instantiation of Parameterized Data Structures for Model-Based Testing. In Jacques Julliand and Olga Kouchnarenko, editors, B'2007, the 7th Int. B Conference, volume 4355 of LNCS, Besancon, France, pages 96--110, January 2007. Springer.

  • Fabrice Bouquet, Frédéric Dadeau, and Julien Groslambert. JML2B: Checking JML specifications with B machines. In Jacques Julliand and Olga Kouchnarenko, editors, B'2007, the 7th Int. B Conference - Tool Session, volume 4355 of LNCS, Besancon, France, pages 285--288, January 2007. Springer.

  • Jean-François Couchot and Frédéric Dadeau. Guiding the Correction of Parameterized Specifications. In IFM'07, 6th Int. Conf. on Integrated Formal Methods, volume 4591 of LNCS, Oxford, UK, pages 176--194, July 2007. Springer.

  • Frédéric Dadeau, Yves Ledru, and Lydie du Bousquet. Directed Random Reduction of Combinatorial Test Suites. In RT'07, 2nd Int. Workshop on Random Testing, co-located with ASE'07, the 22nd IEEE/ACM Int. Conf. on Automated Software Engineering, Atlanta, USA, pages 18--25, November 2007. ACM Press.

  • Frédéric Dadeau, Yves Ledru, and Lydie du Bousquet. Measuring the Coverage of a Java Test Suite using JML Specifications. In B. Finkbeiner, Y. Gurevich, and A.K. Petrenko, editors, MBT'07, 3rd Int. Workshop on Model-Based Testing, co-located with ETAPS'2007), volume 190 of ENTCS, Electronic Notes in Theoretical Computer Science, Braga, Portugal, pages 21--32, April 2007.

  • Yves Ledru, Frédéric Dadeau, Lydie du Bousquet, Sébastien Ville, and Elodie Rose. Mastering Combinatorial Explosion with the Tobias-2 Test Generator. In ASE'07, 22nd IEEE/ACM Int. Conf. on Automated Software Engineering, Tool Session, Atlanta, USA, pages 535--536, November 2007. ACM Press.

  • Yves Ledru, Lydie du Bousquet, Frédéric Dadeau, and F. Allouti. A Case Study in Matching Test and Proof Coverage. In B. Finkbeiner, Y. Gurevich, and A.K. Petrenko, editors, MBT'07, 3rd Int. Workshop on Model-Based Testing, co-located with ETAPS'2007), volume 190 of ENTCS, Electronic Notes in Theoretical Computer Science, Braga, Portugal, pages 73--84, April 2007.

  • Fabrice Bouquet, Frédéric Dadeau, Julien Groslambert, and Jacques Julliand. Safety Property Driven Test Generation from JML Specifications. In K. Havelund, M. Garcia, G. Rosu, and B. Wolff, editors, FATES/RV'06, 1st Int. Workshop on Formal Approaches to Testing and Runtime Verification, volume 4262 of LNCS, Seattle, WA, United States, pages 225--239, August 2006. Springer.

  • Fabrice Bouquet, Frédéric Dadeau, and Bruno Legeard. Automated Boundary Test Generation from JML Specifications. In T. Nipkow and J. Misra, editors, FM'06, 14th Int. Conf. on Formal Methods, volume 4085 of LNCS, Hamilton, Canada, pages 428--443, August 2006. Springer.

  • Fabrice Bouquet, Frédéric Dadeau, and Julien Groslambert. Checking JML Specifications with B Machines. In H. Treharne, S. King, M. Henson, and S. Schneider, editors, Procs of the Int. Conf. on Formal Specification and Development in Z and B, (ZB'05), volume 3455 of LNCS, Guildford, United Kingdom, pages 435--454, April 2005. Springer.

  • Fabrice Bouquet, Frédéric Dadeau, and Bruno Legeard. How Symbolic Animation can help designing an Efficient Formal Model. In K.K. Lau and R. Banach, editors, Procs of the 7th Int. Conf. on Formal Engineering Methods (ICFEM'05), volume 3785 of LNCS, Manchester, United Kingdom, pages 96--110, November 2005. Springer.

  • Fabrice Bouquet, Frédéric Dadeau, and Bruno Legeard. Using Constraint Logic Programming for the Symbolic Animation of Formal Models. In J. Marques-Silva and M. Velev, editors, Procs of the Int. Workshop on Constraints in Formal Verification (CFV'05) -- Co-located with the Int. Conf. on Automated Deduction (CADE'05), Tallinn, Estonia, pages 32--46, July 2005.

  • Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, and Mark Utting. JML-Testing-Tools: a Symbolic Animator for JML Specifications using CLP. In N. Halbwachs and L. Zuck, editors, Procs of the 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems, Tool session (TACAS'05), volume 3440 of LNCS, Edinburgh, United Kingdom, pages 551--556, April 2005. Springer.

  • Fabrice Bouquet, Frédéric Dadeau, Bruno Legeard, and Mark Utting. Symbolic Animation of JML Specifications. In J.S. Fitzgerald, I.J. Hayes, and A. Tarlecki, editors, Procs of the Int. Conf. on Formal Methods (FM'2005), volume 3582 of LNCS, Newcastle Upon Tyne, United Kingdom, pages 75--90, July 2005. Springer.

  • Jean-François Couchot, Frédéric Dadeau, D. Déharbe, Alain Giorgetti, and S. Ranise. Proving and Debugging Set-Based Specifications. In A. Cavalcanti and P. Machado, editors, WMF'03 proceedings, volume 95 of ENTCS, Electronic Notes in Theoretical Computer Science, Campina Grande, Brazil, pages 189--208, May 2004.

National conferences

  • Sébastien Bardin, Bernard Botella, Frédéric Dadeau, Florence Charreteur, Arnaud Gotlieb, Bruno Marre, Claude Michel, Michel Rueher, and Nicky Williams. Constraint-Based Software Testing. In Yves Ledru and M. Pantel, editors, Journées du GDR Génie de la Programmation du Logiciel 2009, Toulouse, France, pages 204--208, January 2009.

  • Frédéric Dadeau. Génération automatique de tests à partir de patrons de propriétés. In AFADL'09, Approches Formelles dans l'Assistance au Développement de Logiciels, Toulouse, France, pages 177--191, January 2009.

  • Frédéric Dadeau, Amal Haddad, and T. Moutet. Test fonctionnel de conformité vis-à-vis d'une politique de contrôle d'accès. In AFADL'07, Approches Formelles dans l'Assistance au Développement de Logiciels, Namur, Belgique, June 2007.

  • Yves Ledru, S. Ville, E. Rose, Lydie du Bousquet, and Frédéric Dadeau. Tobias-2, un outil pour la maîtrise de tests combinatoires. In AFADL'07, Approches Formelles dans l'Assistance au Développement de Logiciels, Session outils, Namur, Belgium, June 2007.

  • Frédéric Dadeau. Animation de modèles JML et génération de tests fonctionnels. In MAJECSTIC'06, MAnifestation de JEunes Chercheurs STIC, Lorient, France, November 2006.

  • Fabrice Bouquet, Frédéric Dadeau, and Bruno Legeard. JML-Testing-Tools, un Animateur Symbolique de Spécifications JML. In AFADL'06, Approches Formelles dans l'Assistance au Développement de Logiciels, Paris, France, March 2006. Note: Session outils.