ForTesSE Publications

2010

• A. Carneiro Viana, S. Maag, and F. Zaïdi. One step forward: Linking wireless self-organising networks validation techniques with formal testing approaches. ACM Computing Survey, 41(3):1-39, to be published 2010. available at http://hal.archives-ouvertes.fr/index.php, HAL: inria-00357655, version 1. [ bib ]
• A. Cavalli, M. Lallali, S. Maag, G. Morales, and F. Zaidi. Emergent Web Intelligence, chapter Modeling and Testing of Web Based Systems. Advanced Information and Knowledge Processing. Springer Verlag, 2010. à paraître Avril 2010, 39 pages. [ bib ]
• Achim D. Brucker, Lukas Brügger, Paul Kearney, and Burkhart Wolff. Verified firewall policy transformations for test case generation. In Ana Cavalli and Sudipto Ghosh, editors, International Conference on Software Testing (ICST10), Lecture Notes in Computer Science. Springer-Verlag, 2010. [ bib | pdf | Abstract ]
• Marc Aiguier and Delphine Longuet. Some general results about proof normalization. Logica Universalis, 2010. To appear. [ bib | pdf | Abstract ]

2009

• Johan Oudinet. Exploration aléatoire de modèles. Journal Européen des Systèmes Automatisés (JESA), 43:905-919, November 2009. Colloque francophone sur la Modélisation des Systèmes Réactifs. [ bib | pdf ]
• L. Bentakouk, P. Poizat, and F. Zaïdi. A formal framework for service orchestration testing based on symbolic transition systems. In TESTCOM/FATES 2009 - 21th IFIP International Conference on Testing of Communicating Systems, Lectures Notes in Computer Science (LNCS), pages 16-32, Eindhoven, November 2009. Springer. [ bib ]
• M.-C. Gaudel, F. Magnez, R. Lassaigne, and M. de Rougemont. Approximations for model checking and testing (survey, preliminary version). 39 pages, under revision, Université de Paris-Sud, May 2009. [ bib | pdf ]
• A. Cavalli, S. Maag, E. Montes de Oca, and F. Zaidi. A formal passive testing approach to test a manet routing protocol. In PWN 2009 5th IEEE PerCom Workshop on Pervasive Wireless Networking, pages 1-6, Texas, March 2009. IEEE. [ bib ]
• F. Zaïdi, A. Cavalli, and E. Bayse. NetworkProtocol Interoperability Testing based on Contextual. In 24th Annual ACM Symposium on Applied on Applied Computing, pages 2-7, Hawaii, USA, March 2009. ACM. [ bib ]
• Achim D. Brucker and Burkhart Wolff. Semantics, calculi, and analysis for object-oriented specifications. Acta Informatica, 46(4):255-284, 2009. [ bib | DOI | pdf | Abstract ]
• Achim D. Brucker and Burkhart Wolff. HOL-TestGen: an interactive test-case generation framework. In Marsha Chechik and Martin Wirsing, editors, Fundamental Approaches to Software Engineering (FASE09), number 5503 in Lecture Notes in Computer Science, pages 417-420. Springer-Verlag, Heidelberg, 2009. [ bib | DOI | pdf | http | .ps.gz | Abstract ]
• Achim D. Brucker, Matthias P. Krieger, and Burkhart Wolff. Extending OCL with null-references. In S. Ghosh, editor, MODELS 2009 Workshops, LNCS 6002, pages 261-275. Springer Verlag, Heidelberg, 2009. Best-Paper Award at the OCL 2009 Workshop. [ bib | pdf | http | .ps.gz | Abstract ]
• Burkhart Wolff. Top-down vs. Bottom-up: Formale Methoden im wissenschaftlichen wettbewerb. Ein essayistischer Survey über den Stand der Kunst. Technical report, DFKI Technischer Bericht, 2009. Erschienen in der Festschrift zum 60. Geburtstag von Bernd Krieg-Brückner. [ bib | pdf ]
• Delphine Longuet and Marc Aiguier. Integration testing from structured first-order specifications via deduction modulo. In International Conference Theoretical Aspects of Computing (ICTAC 2009), volume 5684 of Lecture Notes in Computer Science, pages 261-276. Springer, 2009. [ bib | pdf | Abstract ]
• Delphine Longuet, Marc Aiguier, and Pascale Le Gall. Proof-guided test selection from quantifier-free first-order specifications with equality. Journal of Automated Reasoning, special issue on Tests and Proofs, 2009. To appear. [ bib | pdf | Abstract ]
• Matthias Daum, Jan Dörrenbächer, and Burkhart Wolff. Proving fairness and implementation correctness of a microkernel scheduler. Journal of Automated Reasoning (JAR), 42(2-4):349-388, 2009. G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008). [ bib | DOI | pdf | Abstract ]
• Sascha Böhme, Michal Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie - an interactive prover-backend for the Verified C Compiler. Journal of Automated Resoning (JAR), 44(1-2):111-144, 2009. [ bib | DOI | pdf | Abstract ]

2008

• M. Lallali, F. Zaidi, A. Cavalli, and I. Hwang. Automatic timed test case generation for web services composition. In IEEE Computer Society Press, editor, The 6th IEEE European Conference on Web Services (ECOWS'08), Dublin, November 2008. 53-63. [ bib | pdf ]
• M. Lallali, F. Zaidi, and A. Cavalli. Transforming bpel into intermediate format language for web services composition testing. In 4th International Conference on Next Generation Web Services Practices, Seoul, October 2008. IEEE Computer CS. 191-197. [ bib | pdf ]
• Matthias Daum, Jan Dörrenbächer, Mareike Schmidt, and Burkhart Wolff. A verification approach for system-level concurrent programs. In Verified Software: Theories, Tools, Experiments, LNCS 5295, pages 161-176. Springer Berlin / Heidelberg, September 2008. [ bib | DOI | pdf | Abstract ]
• Achim D. Brucker and Burkhart Wolff. Extensible universes for object-oriented data models. In Jan Vitek, editor, Proceedings of the European Conference of Object-Oriented Programming (ECOOP 2008), LNCS 5142, pages 438-462. Springer-Verlag, Paphos, Cyprus, July 2008. [ bib | DOI | pdf | http | Abstract ]
• Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet, and Sylvain Peyronnet. Coverage-biased random exploration of large models and application to testing. Technical Report 1494, LRI, Université Paris-Sud XI, June 2008. [ bib | pdf ]
• Johan Oudinet. Uniform random exploration of concurrent systems. In MOdelling and VErifying parallel Processes (MOVEP), pages 323-328, June 2008. [ bib ]
• Marie-Claude Gaudel, Alain Denise, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet, and Sylvain Peyronnet. Coverage-biased random exploration of large models. In ETAPS Workshop on Model Based Testing, Electronic Notes in Theoretical Computer Science, March 2008. invited lecture, 11 pages. [ bib | pdf ]
• A. Cavalcanti and M.-C. Gaudel. A note on traces refinement and the conf relation in the Unifying Theories of Programming. In Unifying Theories of Programming 2008, 8th-10th September, Trinity College Dublin,, volume to appear of Lecture Notes in Computer Science. Springer Verlag, 2008. 20 pages. [ bib | pdf ]
• Achim D. Brucker and Burkhart Wolff. An extensible encoding of object-oriented data models in hol with an application to imp++. Journal of Automated Reasoning (JAR), Selected Papers of the AVOCS-VERIFY Workshop 2006(3-4):219-249, 2008. Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds). [ bib | DOI | pdf | Abstract ]
• Achim D. Brucker and Burkhart Wolff. A formal proof environment for uml/ocl. In Proceedings of Formal Aspects of Software Engineering (FASE 2008), volume 4961 of Lecture Notes in Computer Science, pages 97-101. Springer Berlin / Heidelberg, 2008. [ bib | DOI | pdf | Abstract ]
• Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Verifying test-hypotheses - an experiment in test and proof. In Bernd Finkbeiner, Yuri Gurevich, and Alexander K. Petrenko, editors, Model-based Testing (MBT) 2008, volume 202 of Electronic Notes in Theoretical Computer Science, pages 15-28, Budapest, Hungary, 2008. Elsevier Science Publishers. [ bib | DOI | pdf | Abstract ]
• Achim D. Brucker, Lukas Brügger, and Burkhart Wolff. Model-based firewall conformance testing. In Kenji Suzuki and Teruo Higashino, editors, Testcom/FATES 2008, LNCS 5047, pages 103-118. Springer-Verlag, Tokyo, Japan, 2008. [ bib | DOI | pdf | http | Abstract ]
• Carlos Canal, Juan Manuel Murillo, and Pascal Poizat. Practical Approaches for Software Adaptation. Report on the 4th Workshop WCAT at ECOOP 2007. In ECOOP 2007 Workshop Reader, volume 4906 of Lecture Notes in Computer Science, pages 154-165, 2008. [ bib | DOI ]
• Carlos Canal, Pascal Poizat, and Gwen Salaün. Model-based adaptation of behavioural mismatching components. IEEE Transactions on Software Engineering, 34(4):546-563, 2008. [ bib | DOI ]
• Javier Cubo, Gwen Salaün, Carlos Canal, Ernesto Pimentel, and Pascal Poizat. A model-based approach to the verification and adaptation of wf/.net components. In Proceedings of the Workshop on Formal Aspects of Component Software (FACS 07), volume 215 of Electronic Notes in Theoretical Computer Science, pages 39-55. Elsevier, 2008. [ bib | DOI | pdf ]
• Frédérique Bassino, Julien Clément, Julien Fayolle, and Pierre Nicodème. Construction for clumps statistics. In DMTS, 2008. [ bib ]
• J. Fayolle, M.-C. Gaudel, S.-D. Gouraud, and B. Marre. Statistical testing of synchronous reactive systems. In ERTS, 2008. [ bib ]
• Mohammad Mahdi Jaghoori, Delphine Longuet, and Frank S. de Boer. Schedulability and compatibility of real-time asynchronous objects. In 29th IEEE Real-Time Systems Symposium (RTSS 2008), pages 70-79. IEEE Computer Society Press, 2008. [ bib | pdf | Abstract ]
• Julien Fayolle. Analysis of the size of antidictionary in dca. In LNCS, 2008. [ bib ]
• Tarek Melliti, Pascal Poizat, and Sonia Ben Mokhtar. Distributed Behavioural Adaptation for the Automatic Composition of Semantic Services. In Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE 08), volume 4961 of Lecture Notes in Computer Science, pages 146-162. Springer, 2008. [ bib | DOI | pdf ]
• Radu Mateescu, Pascal Poizat, and Gwen Salaün. Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques. In Proceedings of the International Conference on Service Oriented Computing (ICSOC 08), volume 5364 of Lecture Notes in Computer Science, pages 84-99. Springer, 2008. [ bib | DOI ]
• Sandrine Beauche and Pascal Poizat. Automated Service Composition with Adaptive Planning. In Proceedings of the International Conference on Service Oriented Computing (ICSOC 08), volume 5364 of Lecture Notes in Computer Science, pages 530-537. Springer, 2008. [ bib | DOI | pdf ]
• Sascha Böhme, Rustan Leino, and Burkhart Wolff. Hol-boogie - an interactive prover for the boogie program verifier. In Sofiene Tahar, Otmane Ait Mohamed, and César Muñoz, editors, 21th International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2008), LNCS 5170. Springer-Verlag, Montreal, Canada, 2008. [ bib | DOI | pdf | Abstract ]

2007

• M. Lallali, F. Zaidi, and A. Cavalli. Timed modeling of web services composition for automatic testing. In SITIS IEEE/ACM 2007, pages 417-427, Shanghai, December 2007. IEEE Computer Society. [ bib | pdf ]
• Johan Oudinet. Uniform random walks in very large models. In RT '07: Proceedings of the 2nd international workshop on Random testing, pages 26-29, Atlanta, GA, USA, November 2007. ACM Press. [ bib | pdf | slides | Abstract ]
• Johan Oudinet. Uniform random walks in concurrent models. Master's thesis, Université Paris-Sud 11, LRI, September 2007. [ bib | pdf ]
• Johan Oudinet. Tirages aléatoires uniformes dans des systèmes concurrents. Master's thesis, Université Paris-Sud 11, LRI, September 2007. [ bib | pdf | slides | Abstract ]
• M. Lallali, F. Zaidi, and A. Cavalli. Timed modeling of web services composition for automatic testing. Technical Report 07008-LOR, GET/INT, Evry, September 2007. Long version. [ bib ]
• David Basin, Hironobu Kuruma, Shin Nakajima, and Burkhart Wolff. The z specification language and the proof environment isabelle/hol-z. Computer Software - Journal of the Japanese Society for Software Science and Technology, 24(2):21-26, April 2007. In Japanese. [ bib | http | Abstract ]
• David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi, and Burkhart Wolff. Verifying a signature architecture: a comparative case study. Formal Aspects of Computing, 19(1):63-91, March 2007. http://www.springerlink.com/content/u368650p18557674/?p=8851693f5ba14a3fb9d493dae37783b8&pi=0. [ bib | DOI | pdf | Abstract ]
• A. Cavalcanti and M.-C. Gaudel. Testing for refinement in CSP. In Formal Methods and Software Engineering, ICFEM 2007, volume 4789 of Lecture Notes in Computer Science, pages 151-170. Springer Verlag, 2007. [ bib | pdf ]
• Achim D. Brucker and Burkhart Wolff. Test-sequence generation with hol-testgen - with an application to firewall testing. In Bertrand Meyer and Yuri Gurevich, editors, TAP 2007: Tests And Proofs, number 4454 in Lecture Notes in Computer Science, pages 149-168. Springer-Verlag, Zurich, 2007. [ bib | DOI | pdf | http | .ps.gz | Abstract ]
• Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. An MDA framework supporting OCL. Electronic Communications of the EASST, 5, 2007. [ bib | pdf | http | Abstract ]
• Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. Semantic issues of OCL: Past, present, and future. Electronic Communications of the EASST, 5, 2007. [ bib | pdf | http | Abstract ]
• Marc Aiguier, Agnès Arnould, Pascale Le Gall, and Delphine Longuet. Test selection criteria for quantifier-free first-order specifications. In International Symposium on Fundamentals of Software Engineering (FSEN 2007), volume 4767 of Lecture Notes in Computer Science, pages 144-159. Springer, 2007. [ bib | pdf | Abstract ]
• Marc Aiguier and Delphine Longuet. Test selection criteria for modal specifications of reactive systems. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007), pages 159-170, 2007. [ bib | pdf | Abstract ]
• Christian Attiogbé, Pascal Poizat, and Gwen Salaün. A formal and tool-equipped approach for the integration of state diagrams and formal datatypes. IEEE Transactions on Software Engineering, 33(3):157-170, 2007. [ bib | DOI ]
• Steffen Becker, Carlos Canal, Nikolay Diakov, Juan Manuel Murillo, Pascal Poizat, and Massimo Tivoli. Coordination and adaptation techniques: Bridging the gap between design and implementation. In ECOOP 2006 Workshop Reader, volume 4379 of Lecture Notes in Computer Science, pages 72-86. Springer, 2007. [ bib | DOI ]
• Javier Cubo, Gwen Salaün, Carlos Canal, Ernesto Pimentel, and Pascal Poizat. Relating model-based adaptation and implementation platforms: A case study with wf/.net 3.0. In Proceedings of the 12th International Workshop on Component-Oriented Programming (WCOP 07), volume 182 of Electronic Notes in Theoretical Computer Science, pages 9-13. Elsevier, 2007. [ bib | pdf ]
• F. Zaidi and Mounir Lallali. Use of verification techniques for components testing. Technical Report 1465, LRI, http://www.lri.fr/Rapports-internes, Université Paris-Sud XI, January 2007. [ bib ]
• Frédérique Bassino, Julien Clément, Julien Fayolle, and Pierre Nicodème. Counting occurrences for a finite set of words: an inclusion-exclusion approach algorithms. In Philippe Jacquet, editor, Proceedings of the 2007 International Conference on Analysis of Algorithms, pages 95-104. DMTCS, 2007. [ bib ]
• Serge Haddad and Pascal Poizat. Transactional reduction of component compositions. In Proceedings of the IFIP International Conference on Formal Methods for Networked and Distributed Systems (FORTE 07), volume 4574 of Lecture Notes in Computer Science, pages 341-357. Springer, 2007. [ bib | DOI | pdf ]
• Delphine Longuet. Test à partir de spécifications axiomatiques. PhD thesis, Laboratoire IBISC, Université d'Évry-Val d'Essonne, 2007. [ bib | pdf | Abstract ]
• Delphine Longuet and Marc Aiguier. Specification-based testing for CoCasl's modal specifications. In Second International Conference on Algebra and Coalgebra in Computer Science (CALCO 2007), volume 4624 of Lecture Notes in Computer Science, pages 356-371. Springer, 2007. [ bib | pdf | Abstract ]
• M.-C. Gaudel and P. Le Gall. Testing data types implementations from algebraic specifications. In Formal Methods and Testing, R. Hierons, J. Bowen, and M. Harman,eds, volume 4949 of Lecture Notes in Computer Science. Springer-Verlag, 2007. 209-239. [ bib | pdf ]
• Makarius Wenzel and Burkhart Wolff. Building formal method tools in the isabelle/isar framework. In Klaus Schneider and Jens Brandt, editors, TPHOLs 2007, LNCS 4732, pages 351-366. Springer-Verlag, 2007. [ bib | DOI | pdf | Abstract ]
• Radu Mateescu, Pascal Poizat, and Gwen Salaün. Behavioral adaptation of component compositions based on process algebra encodings. In Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 07), pages 385-388. ACM,IEEE, 2007. [ bib | DOI | pdf ]
• Nicolas Baskiotis, Michèle Sebag, Marie-Claude Gaudel, and Sandrine-Dominique Gouraud. A machine learning approach for statistical software testing. In IJCAI, Proceedings of the 20th International Joint Conference on Artificial Intelligence, pages 2274-2279, 2007. [ bib | pdf ]
• Pascal Poizat and Gwen Salaün. Adaptation of open component-based systems. In Proceedings of the IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 07), volume 4468 of Lecture Notes in Computer Science, pages 141-156. Springer, 2007. [ bib | DOI | pdf ]
• Pascal Poizat, Gwen Salaün, and Massimo Tivoli. An adaptation-based approach to incrementally build component systems. In Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 06), volume 182 of Electronic Notes in Theoretical Computer Science, pages 155-170. Elsevier, 2007. [ bib | DOI | pdf ]

2006

• S. Maag and F. Zaidi. A step-wise validation approach for a wireless routing protocol. In IEEE International Conference on Communications and Electronics (ICCE'06), Hanoi, Vietnam, October 2006. IEEE. [ bib ]
• S. Maag and F. Zaidi. Spécification formelle pour le test d'un protocole de routage ad hoc. Technical Report 06009-LOR, GET/INT, France, October 2006. [ bib ]
• Achim D. Brucker and Burkhart Wolff. A package for extensible object-oriented data models with an application to imp++. In Abhik Roychoudhury and Zijiang Yang, editors, International Workshop on Software Verification and Validation (SVV 2006), Computing Research Repository (CoRR). Seattle, USA, August 2006. [ bib | pdf | .ps.gz | Abstract ]
• A. Denise, M.-C. Gaudel, S.-D. Gouraud, R. Lassaigne, and S. Peyronnet. Uniform random sampling of traces in very large models. In 1st International ACM Workshop on Random Testing, pages 10 -19, July 2006. [ bib | pdf ]
• Manuel Núñez García, Klaus Havelund, Grigore Rosu, and Burkhart Wolff, editors. Proceedings of the International Workshop on Formal Aspects of Testing and Runtime Verification (FATES/RV), Seattle, USA, 2006. Springer Verlag. LNCS 4262. [ bib | DOI | Abstract ]
• A. Denise, M.-C. Gaudel, S.-D. Gouraud, R. Lassaigne, and S. Peyronnet. Uniform random sampling of traces in very large models. In 1st ACM International Workshop on Random Testing (RT), pages 10-19, 2006. [ bib ]
• A. Denise, M.-C. Gaudel, S.-D. Gouraud, R. Lassaigne, and S. Peyronnet. Uniform random sampling of traces in very large models. Technical Report 1445, Université Paris-Sud 11, 2006. [ bib | pdf ]
• Achim D. Brucker and Burkhart Wolff. The hol-ocl book. Technical Report 525, ETH Zürich, 2006. [ bib | pdf | Abstract ]
• Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. An MDA framework supporting OCL. In 6th OCL Workshop at the UML/MoDELS Conference, 2006. [ bib | pdf | Abstract ]
• Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. Semantic issues of OCL: Past, present, and future. In 6th OCL Workshop at the UML/MoDELS Conference, 2006. [ bib | pdf | http | Abstract ]
• Achim D. Brucker, Jürgen Doser, and Burkhart Wolff. A model transformation semantics and analysis methodology for SecureUML. In Oscar Nierstrasz, Jon Whittle, David Harel, and Gianna Reggio, editors, MoDELS 2006: Model Driven Engineering Languages and Systems, LNCS 4199, pages 306-320. Springer-Verlag, Genova, 2006. An extended version of this paper is available as ETH Technical Report, no. 524. [ bib | DOI | Abstract ]
• Marc Aiguier, Diane Bahrami, and Delphine Longuet. An abstract way to define rewriting logic. In IPM International Workshop on Foundations of Software Engineering (FSEN 2005), volume 159 of Electronic Notes in Theoretical Computer Science, pages 205-226, 2006. [ bib | pdf | Abstract ]
• Carlos Canal, Juan Manuel Murillo, and Pascal Poizat. Software adaptation. L'Objet, 12(1):9-31, 2006. [ bib | pdf ]
• Carlos Canal, Pascal Poizat, and Gwen Salaün. Synchronizing behavioural mismatch in software composition. In Proceedings of the 8th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), volume 4037 of Lecture Notes in Computer Science, pages 63-77, 2006. [ bib | DOI | pdf ]
• Carlos Canal, Pascal Poizat, and Gwen Salaün. Adaptation de composants logiciels. une approche automatisée basée sur des expressions régulières de vecteurs de synchronisation. In Actes de la Première Conférence Francophone sur les Architectures Logicielles (CAL), 2006. [ bib ]
• Marc Frappier, Henri Habrias, and Pascal Poizat. Software Specification Methods: an Overview Using a Case Study, chapter 19 - A Comparison of the Specification Methods. ISTE, Hermes Science Publishing, 2006. [ bib ]
• G. Lestiennes and M.-C. Gaudel. Modélisation et test de systèmes comportant des actions prioritaires. Rapport LRI 1434, Université de Paris-Sud, march 2006. [ bib | pdf ]
• M.-C. Gaudel. Validation et vérification. In Encyclopédie de l'informatique et des systèmes d'information, pages 1136-1150. Vuibert, 2006. [ bib ]
• M.-C. Gaudel. Les objets à l'épreuve des faits. In Communication, Connaissance : supports et médiations à l'âge de l'information, J.-G. Ganascia, ed. CNRS Éditions, 2006. 4 pages. [ bib ]
• Henri Habrias, Pascal Poizat, and Marc Frappier. Software Specification Methods: an Overview Using a Case Study, chapter 20 - Glossary. ISTE, Hermes Science Publishing, 2006. [ bib ]
• Julien Fayolle. Compression de données sans perte et combinatoire analytique. PhD thesis, Université Paris VI, 2006. [ bib ]
• Pascal Poizat. Software Specification Methods: an Overview Using a Case Study, chapter 12 - SDL. ISTE, Hermes Science Publishing, 2006. [ bib ]
• Pascal Poizat and Jean-Claude Royer. A formal architectural description language based on symbolic transition systems and modal logic. Journal of Universal Computer Science (J.UCS), 12(12):1741-1782, 2006. [ bib | pdf ]
• Pascal Poizat, Jean-Claude Royer, and Gwen Salaün. Bounded analysis and decomposition for behavioural descriptions of components. In Proceedings of the 8th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS), volume 4037 of Lecture Notes in Computer Science, pages 33-47, 2006. [ bib | DOI | pdf ]
• Pascal Poizat, Gwen Salaün, and Massimo Tivoli. On dynamic reconfiguration of behavioural adaptation. In Proceedings of the third International Workshop on Coordination and Adaptation Techniques for Software Entities (WCAT 06), pages 61-69, 2006. [ bib | pdf ]
• Pascal Poizat and Thomas Vergnaud. Méthodes formelles pour les systèmes répartis et coopératifs, chapter 5 - Langages de description d'architecture. Hermes, Lavoisier, 2006. [ bib ]
• S. Maag and F. Zaidi. Testing methodology for an ad hoc routing protocol. In PM2HW2N '06: Proceedings of the ACM international workshop on Performance monitoring, measurement, and evaluation of heterogeneous wireless and wired networks, pages 48-55, Terromolinos, Spain, 2006. ACM. http://doi.acm.org/10.1145/1163653.1163663. [ bib | pdf ]
• S.-D. Gouraud and A. Gotlieb. Using chrs to generate functional test cases for the java card virtual machine. In 8th International Symposium on Practical Aspects of Declarative Languages (PADL), LNCS 3819, pages 1-15, 2006. [ bib | pdf ]

2005

• A. Cavalli, S. Maag, and F. Zaidi. Une approche uml pour la validation des services web. In 5ème Colloque international sur les NOuvelles TEchnologies de la REpartition (NOTERE), September 2005. [ bib | pdf ]
• A. Cavalli, A. Mederreg, F. Zaidi, P. Combes, W. Monin, R. Castanet, M. MacKaya, and P. Laurencot. Une Plate-forme de Validation Multi-Services et Multi-Protocoles - Résultats d'Expérimentations. Annales des Télécommunications, 60(5-6):588-609, June 2005. [ bib ]
• Achim D. Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 user guide. Technical Report 482, Computer Security Group, ETH Zürich, apr 2005. [ bib ]
• Achim D. Brucker and Burkhart Wolff. Interactive testing using HOL-TestGen. In Wolfgang Grieskamp and Carsten Weise, editors, Formal Approaches to Testing of Software (FATES 05), LNCS 3997, pages 87-102. Springer-Verlag, Edinburgh, 2005. [ bib | DOI | Abstract ]
• Achim D. Brucker and Burkhart Wolff. Symbolic test case generation for primitive recursive functions. In Jens Grabowski and Brian Nielsen, editors, Formal Approaches to Testing of Software (FATES 04), LNCS 3395, pages 16-32. Springer-Verlag, Linz 04, 2005. [ bib | DOI | http | Abstract ]
• Achim D. Brucker and Burkhart Wolff. A verification approach for applied system security. International Journal on Software Tools for Technology Transfer (STTT), 7(3):233-247, 2005. [ bib | DOI | pdf | Abstract ]
• Marc Aiguier, Pascale Le Gall, Delphine Longuet, and Assia Touil. A temporal logic for input output symbolic transition systems. In 12th Asia-Pacific Software Engineering Conference (APSEC 2005), pages 43-50, 2005. [ bib | pdf | Abstract ]
• Burkhart Wolff. Correct tools for formal methods in software engineering, 2005. Habilitationsschrift. [ bib | .pdf | Abstract ]
• C. Jones, D. Lomet, A. Romanovsky, G. Weikum, A. Fekete, M.-C. Gaudel, H. F. Korth, R. de Lemos, E. Moss, R. Rajwar, K. Ramamritham, B. Randell, and L. Rodrigues. The atomic manifesto: a story in four quarks. Journal of Universal Computer Science, 11(5):636-650, 2005. [ bib | pdf ]
• Carlos Canal, Juan Manuel Murillo, and Pascal Poizat. Coordination and adaptation techniques for software entities. In European Conference on Object-Oriented Programming (ECOOP) 2004 Workshop Reader, volume 3344 of Lecture Notes in Computer Science, pages 133-147, 2005. [ bib | DOI | pdf ]
• David Aspinall, Christoph Lüth, and Burkhart Wolff. Assisted proof document authoring. In Fourth International Conference on Mathematical Knowledge Management (MKM 05), LNCS 3863. Springer Verlag, 2005. [ bib | DOI | Abstract ]
• David Basin, Hironobu Kuruma, Kazuo Takaragi, and Burkhart Wolff. Specifying and verifying hysteresis signature system with hol-z. Technical Report 471, Computer Security Group, ETH Zürich, 1 2005. [ bib | pdf | Abstract ]
• David Basin, Hironobu Kuruma, Kazuo Takaragi, and Burkhart Wolff. Verification of a signature architecture with hol-z. In Formal Methods 2005, LNCS 3582, pages 269-285. Springer Verlag, 2005. [ bib | DOI | Abstract ]
• E. Bayse, A. Cavalli, M. Nunez, and F. Zaidi. A passive testing approach based on invariants: application to the wap. In Computer Networks, volume 48, pages 247-266. Elsevier Science, 2005. [ bib | pdf ]
• G. Lestiennes and M.-C. Gaudel. Test de systèmes réactifs non réceptifs. Journal Europén des Systèmes automatisés, 36(1-2-3):255-270, 2005. proceedings of MSR'05. [ bib | pdf ]
• M.-C. Gaudel. Toward undoing in composite web services. In Architecting Dependable Systems III, volume 3549 of Lecture Notes in Computer Science, pages 59-68. Springer Verlag, 2005. [ bib | pdf ]
• M.-C. Gaudel. Formal methods and testing: Hypotheses, and correctness approximations. In FM 2005: Formal Methods: International Symposium of Formal Methods, volume 3582 of Lecture Notes in Computer Science, pages 2-8. Springer Verlag, 2005. keynote talk. [ bib | pdf ]
• Julien Fayolle and Mark Daniel Ward. Analysis of the average depth in a suffix tree under a markov model. In Conrado Martínez, editor, Proceedings of the 2005 International Conference on the Analysis of Algorithms, pages 95-104. DMTCS, 2005. Proceedings of a colloquium organized by Universitat Politècnica de Catalunya, Barcelona, Catalunya, June 2005. [ bib ]
• Delphine Longuet. Une théorie du raffinement orientée propriétés pour les automates communicants. Master's thesis, Laboratoire de Méthodes Informatiques (LaMI), Université d'Évry-Val d'Essonne, 2005. [ bib | pdf | Abstract ]
• Sebastian Pavel, Jacques Noyé, Pascal Poizat, and Jean-Claude Royer. Java implementation of a component model with explicit symbolic protocols. In Software Composition (SC), volume 3628 of Lecture Notes in Computer Science, pages 115-124, 2005. [ bib | DOI | pdf ]
• S.-D. Gouraud. Auguste: a tool for statistical testing (experimental results). Technical Report 1400, Université Paris-Sud 11, 2005. [ bib | pdf ]
• S.-D. Gouraud and A. Gotlieb. Utilisation des chrs pour générer des cas de test pour la machine virtuelle java card. In Journées Francophones de Programmation par Contraintes (JFPC), pages 383-392, 2005. [ bib | pdf ]
• S.-D. Gouraud and A. Gotlieb. Using chrs to generate functional test cases for the java card virtual machine. Technical Report 1725, 2005. [ bib | pdf ]
• Gwen Salaün and Pascal Poizat. Interacting extended state diagrams. In Proceedings of the International Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 04), volume 115 of Electronic Notes in Theoretical Computer Science, pages 49-57. Elsevier, 2005. [ bib | DOI | pdf ]
• Thomas Meyer and Burkhart Wolff. Tactic-based optimized compilation of functional programs. In Jean-Christophe Filliatre, Christine Paulin, and Benjamin Werner, editors, Types for Proofs and Programs (TYPES 2004), LNCS 3839, pages 202-215. Springer Verlag, 8 2005. [ bib | DOI | pdf | Abstract ]

2004

• A. Cavalli, A. Mederreg, and F. Zaïdi. Application of a formal testing methodology to wireless telephony networks. International Journal of the Brazilian Computer Society (JCBS), 10(2):56-68, November 2004. ISSN 0104-6500. [ bib ]
• A. Cavalli, S. Maag, S. Papagiannaki, G. Vergiakis, and F. Zaïdi. A Testing Methodology for an Open Software E-Learning Platform. In 18th IFIP World Computer congress-TC10/WG10.5 Workshop Edutech, pages 165-174, Toulouse, France, August 2004. [ bib ]
• A. Cavalli, A. Mederreg, F. Zaidi, P. Combes, W. Monin, R. Castanet, M. Mackaya, and P. Laurencot. A multi-service and multi-protocol validation platform experimentation results. In R. Hierons and R. Groz, editors, Testing of Communicating Systems (Testcom'04), LNCS 2978, pages 17-19. The 16th IFIP International Conference, TestCom, Springer, March 2004. [ bib ]
• A. Denise, M.-C. Gaudel, and S.-D. Gouraud. A generic method for statistical testing. In 15th. IEEE International Symposium on Software Reliability Engineering (ISSRE), pages 25-34, 2004. [ bib | pdf ]
• A. Denise, M.-C. Gaudel, and S.-D. Gouraud. A generic method for statistical testing. Technical Report 1386, 2004. [ bib ]
• A. Denise, M.-C. Gaudel, and S.-D. Gouraud. A generic method for statistical testing. In IEEE Int. Symp. on Software Reliability Engineering (ISSRE), pages 25-34, 2004. [ bib | pdf ]
• Achim D. Brucker and Burkhart Wolff. Symbolic test case generation for primitive recursive functions. Technical Report 449, Computer Security Group, ETH Zürich, jun 2004. [ bib | Abstract ]
• Julien Fayolle. An average-case analysis of basic parameters of the suffix tree. In Michael Drmota, Philippe Flajolet, Danièle Gardy, and Bernhard Gittenberger, editors, Mathematics and Computer Science, pages 217-227. Birkhäuser, 2004. Proceedings of a colloquium organized by TU Wien, Vienna, Austria, September 2004. [ bib ]
• Nicole Rauch and Burkhart Wolff. Formalizing java's two's-complement integral type in isabelle/hol. Technical Report 458, ETH Zürich, 11 2004. [ bib | pdf | Abstract ]
• S.-D. Gouraud. Auguste: un outil pour le test statistique. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), pages 337-340, 2004. [ bib ]
• S.-D. Gouraud. Utilisation des Structures Combinatoires pour le Test Statistique. PhD thesis, Université Paris-Sud 11, LRI, 2004. [ bib | pdf ]

2003

• A. Cavalli, A. Mederreg, and F. Zaïdi. Application of formal testing methodology to wireless telephony networks. In 2nd International Information and Telecommunications TEchnologies Symposium, I2TS'2003, Florianopolis, Brazil, October 2003. [ bib ]
• A. Mederreg, F. Zaïdi, P. Combes, W. Monin, R. Castanet, M. MacKaya, and P. Laurencot. Une Plate-forme de Validation Multi-Services et Multi-Protocoles - Résultats d'Expérimentations. In M. Riguidel et A. Serhouchni A. Cavalli, editor, CFIP'2003 Ingénierie des Protocoles, pages 135-151, Paris, October 2003. Hermès. [ bib ]
• C. Besse, A. Cavalli, and F. Zaïdi. Génération de tests d'interopérabilité pour le protocole tcp. In 4ème Colloque Francophone sur la Modélisation des Systèmes Réactifs, Metz, October 2003. Hermès. [ bib ]
• Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. Hol-z 2.0: A proof environment for z-specifications. Journal of Universal Computer Science, 9(2):152-172, February 2003. [ bib | DOI | pdf | .ps.gz | Abstract ]
• David Basin and Burkhart Wolff, editors. Theorem Proving in Higher Order Logics, 16th International Conference (TPHOLs 2003), Rome, Italy, Sep 2003. Springer-Verlag. LNCS 2758. [ bib | DOI | Abstract ]
• Fatiha Zaïdi. Platonis - rapport final. Delivrable, Institut National des Télécommunications, France, 2003. [ bib ]
• Achim D. Brucker and Burkhart Wolff. Using theory morphisms for implementing formal methods tools. In Herman Geuvers and Freek Wiedijk, editors, Types 2002, Proceedings of the workshop Types for Proof and Programs, LNCS 2646. Springer-Verlag, Nijmegen, 2003. [ bib | DOI | Abstract ]
• Achim D. Brucker and Burkhart Wolff. A case study of a formalized security architecture. In Thomas Arts and Wan Fokkink, editors, Eighth International Workshop onFormal Methods for Industrial Critical Systems (FMICS'03), volume 80. Elsevier Science Publishers, 2003. [ bib | pdf | .ps.gz | Abstract ]
• Nicole Rauch and Burkhart Wolff. Formalizing java's two's-complement integral type in isabelle/hol. In Electronic Notes in Theoretical Computer Science, volume 80. Elsevier Science Publishers, 2003. [ bib | pdf | Abstract ]
• S.-D. Gouraud. Génération de tests à l'aide d'outils combinatoires: Premiers résultats expérimentaux. Technical Report 1364, 2003. [ bib | pdf ]

2002

• A. Cavalli, A. Mederreg, and F. Zaïdi. Mobiles services validation. In Nagib Callaos and al, editors, The 6th World Conference on Systemics, Cybernics and Informatics, Orlando, July 2002. IIIS. [ bib ]
• Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. The CVS-server case study: A formalized security architecture. In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors, FM-TOOLS 2002, number 2002-11 in Technical Report, pages 47-52. Augsburg, July 2002. [ bib | pdf | http | Abstract ]
• Achim D. Brucker, Stefan Friedrich, Frank Rittinger, and Burkhart Wolff. HOL-Z 2.0: A proof environment for z-specifications. In Dominik Haneberg, Gerhard Schellhorn, and Wolfgang Reif, editors, FMTOOLS 2002, number 2002-11 in Technical Report, pages 33-38. Augsburg, July 2002. [ bib | pdf | http | Abstract ]
• Cédric Besse, Ana R. Cavalli, Myungchul Kim, and Fatiha Zaïdi. Automated generation of interoperability tests. In FIP/TC6/WG6.1 Fourteenth International Conference on Testing of Communicating Systems (Testcom 2002), pages 169-184, Berlin, March 2002. Kluwer Academic. ISBN 0-7923-7695-1. [ bib ]
• Fatiha Zaïdi. Mise en place du réseau d'expérimentations. Delivrable platonis-fc-t13/d13, Institut National des Télécommunications, France, 2002. [ bib ]
• Achim D. Brucker and Burkhart Wolff. HOL-OCL: Experiences, consequences and design choices. In Jean-Marc Jézéquel, Heinrich Hussmann, and Stephen Cook, editors, UML 2002: Model Engineering, Concepts and Tools, number 2460 in Lecture Notes in Computer Science. Springer-Verlag, Dresden, 2002. [ bib | DOI | pdf | http | Abstract ]
• Achim D. Brucker and Burkhart Wolff. A proposal for a formal OCL semantics in Isabelle/HOL. In César Muñoz, Sophiène Tahar, and Víctor Carreño, editors, Theorem Proving in Higher Order Logics, number 2410 in Lecture Notes in Computer Science, pages 99-114. Springer-Verlag, Hampton, VA, USA, 2002. [ bib | DOI | pdf | http | Abstract ]
• Achim D. Brucker, Frank Rittinger, and Burkhart Wolff. A CVS-Server security architecture - concepts and formal analysis. Technical Report 182, Albert-Ludwigs-Universität Freiburg, 2002. [ bib | pdf | http | .ps.gz | Abstract ]
• Burkhart Wolff, Oliver Berthold, Sebastian Clauß, Hannes Federrath, Stefan Köpsell, and Andreas Pfitzmann. Towards a formal analysis of a mix network. Technical Report 171, Albert-Ludwigs-Universität Freiburg, 2002. [ bib | pdf ]
• Julien Fayolle. Paramètres des arbres suffixes dans le cas de sources simples, 2002. Mémoire de DEA, Université Paris VI. [ bib ]
• G. Lestiennes and M.-C. Gaudel. Testing processes from formal specifications with inputs, outputs, and datatypes. In IEEE Int. Symp. on Software Reliability Engineering (ISSRE), pages 3-14, 2002. [ bib | pdf ]

2001

• Achim D. Brucker and Burkhart Wolff. Testing distributed component based systems using UML/OCL. In K. Bauknecht, W. Brauer, and Th. Mück, editors, Informatik 2001, volume 1 of Tagungsband der GI/ÖCG Jahrestagung, pages 608-614, Wien, November 2001. Österreichische Computer Gesellschaft. [ bib | pdf | http | .ps.gz | Abstract ]
• F. Zaïdi. Open problems in protocol testing. Workshop on protocol and dsitributed systems testing, October 2001. Université de Campinas, Brésil. [ bib ]
• A. Cavalli, B. Defude, Ch. Rinderknecht, and F. Zaïdi. A Service-Component Testing Method adn Suitable CORBA Architecture. In IEEE Computer Society, editor, Proceedings of the Sixth IEEE Symposium on Computers and Communications, pages 655-660, Tunisia, July 2001. [ bib ]
• Achim D. Brucker and Burkhart Wolff. Checking OCL Constraints in Distributed Systems Using J2EE/EJB. Technical Report 157, Albert-Ludwigs-Universität Freiburg, July 2001. [ bib | pdf | http | .ps.gz | Abstract ]
• Christoph Lüth and Burkhart Wolff. sml_tk: Functional programming for guis - reference manual. Technical Report 158, Albert-Ludwigs-Universität Freiburg, July 2001. [ bib | pdf | Abstract ]
• Burkhart Wolff. Verifying explicit substitution calculi in binding structures with effect binding. In Pierre Lescanne, editor, Workshop on Explicit Substitution Theory and Applications (WESTAPP'01), volume 210 of Logic Group Preprint Series, pages 58 - 71. Department of Philosophy - Utrecht University, May 2001. [ bib | .ps.gz | Abstract ]
• Fatiha Zaïdi. Test du service rpvm. Delivrable fc-t222, Institut National des Télécommunications, France, 2001. [ bib ]
• S.-D. Gouraud. Application de la génération aléatoire de structures combinatoires au test de logiciel. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL), pages 99-112, 2001. [ bib | pdf ]
• S.-D. Gouraud, A. Denise, M.-C. Gaudel, and B. Marre. A new way of automating statistical testing methods. In 16th. IEEE International Conference on Automated Software Engineering (ASE), pages 5-12, 2001. [ bib | pdf ]
• S.-D. Gouraud, A. Denise, M.-C. Gaudel, and B. Marre. A new way of automating statistical testing methods. Technical Report 1290, 2001. [ bib ]
• S.-D. Gouraud, A. Denise, M.-C. Gaudel, and B. Marre. A new way of automating statistical testing methods. In IEEE International Conference on Automated Software Engineering (ASE), pages 5-12, 2001. [ bib | pdf ]

2000

• A. Cavalli, B. Defude, Ch. Rinderknecht, and F. Zaïdi. Test de composants de service et exécution de tests sur une plateforme corba. In Michel Diaz Patrick Sénac Jean-Pierre Courtiat, editor, CFIP'2000 Ingénierie des protocoles, pages 363-378, Toulouse, October 2000. Hermès. [ bib ]
• T. Meyer and Burkhart Wolff. Correct code-generation in a generic framework. In M. Aargaard, J. Harrison, and T. Schubert, editors, TPHOLs 2000: Supplemental Proceedings, OGI Technical Report CSE 00-009, pages 213-230. Oregon Graduate Institute, Portland, USA, July 2000. [ bib | pdf | .ps.gz | Abstract ]
• F. Zaïdi and A. Cavalli. Tutorial: Automatic embedded test generation. université de reims. International Conference on Software Engineering Applied to Networking and Parallel/Distributed Computing (SNPD'2000), May 2000. [ bib ]
• Christoph Lüth and Burkhart Wolff. More about TAS and IsaWin: Tools for formal program development. In T. Maibaum, editor, Fundamental Approaches to Software Engineering FASE 2000. Joint European Conferences on Theory and Practice of Software ETAPS 2000, number 1783 in Lecture Notes in Computer Science, pages 367- 370. Springer Verlag, 2000. [ bib | pdf | .ps.gz | Abstract ]
• Christoph Lüth and Burkhart Wolff. TAS - a generic window inference system. In J. Harrison and M. Aagaard, editors, Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000, number 1869 in Lecture Notes in Computer Science, pages 405-422. Springer Verlag, 2000. [ bib | pdf | .ps.gz | Abstract ]
• David Basin, Luca Viganò, and Burkhart Wolff. Berichte aus den instituten: Lehrstuhl für softwaretechnik und softwareproduktionsumgebung, freiburg. PIK (Praxis der Informationsverarbeitung und Kommunikation), 23(4):248-249, 2000. [ bib | pdf | .ps.gz ]
• S.-D. Gouraud. Application des techniques de génération aléatoire au test de logiciel, 2000. [ bib | pdf ]

1999

• Ana Cavalli, David Lee, Christian Rinderknecht, and Fatiha Zaïdi. Un algorithme pour le test imbriqué avec des applications aux services r.i. In Actes de la 3ème édition des journées Doctorales Informatique et Réseaux, pages 22-24, Insitut National des Télécommunications, Evry, November 1999. [ bib ]
• A. Cavalli, D. Lee, C. Rinderknecht, and F. Zaïdi. Hit-or-Jump: An algorithm for Embedded Testing with Applications to In Services. In Jianping Wu and al., editors, Proceeding of IFIP International conference FORTE/PSTV'99, pages 41-56, Beijing, China, October 1999. [ bib ]
• Christoph Lüth and Burkhart Wolff. Functional design and implementation of graphical user interfaces for theorem provers. Journal of Functional Programming, 9(2):167- 189, 1999. [ bib | DOI | pdf | .ps.gz | Abstract ]
• P. R. James, M. Endler, and M.-C. Gaudel. Development of an atomic broadcast protocol using LOTOS. Software Practice and Experience, 29(8):699-719, 1999. [ bib ]

1998

• C. Lüth, E. W. Karlsen, Kolyang, S. Westmeier, and B. Wolff. Tool integration in the uniform workbench. In Berghammer and Hoffmann, editors, Workshop on Tool Support for System Specification, Development, and Verification, 1998. [ bib | .ps.gz | Abstract ]
• Chritoph Lüth, Einar W. Karlsen, Kolyang, Stefan Westmeier, and Burkhart Wolff. HOL-Z in the UniForM-Workbench - a case study in tool integration for z. In J. Bowen, editor, 11. International Conference of Z Users ZUM'98, LNCS 1493, pages 116-134. Springer Verlag, 1998. [ bib | DOI | .ps.gz | Abstract ]
• M.-C. Gaudel and P. R. James. Testing algebraic data types and processes: a unifying theory. Formal Aspects of Computing, 10(5-6):436-451, 1998. [ bib | pdf ]

1997

• B. Wolff. A Generic Calculus of Transformations. PhD thesis, Universität Bremen, Aachen, 1997. [ bib | www: | Abstract ]
• H. Tej and B. Wolff. A corrected failure-divergence model for csp in isabelle/hol. In J. Fitzgerald, C.B. Jones, and P. Lucas, editors, Proceedings of the FME 97 - Industrial Applications and Strengthened Foundations of Formal Methods, LNCS 1313, pages 318-337. Springer Verlag, 1997. [ bib | DOI | pdf | .ps.gz | Abstract ]
• Kolyang, C. Lüth, T. Meier, and B. Wolff. Tas and isawin: Generic interfaces for transformational program development and theorem proving. In M. Dauchet M. Bidoit, editor, TAPSOFT 97: Theory and Practice of Software Development, LNCS 1214, pages 855-858. Springer Verlag, 1997. [ bib | DOI | .ps.gz ]
• Kolyang, C. L}uth, T. Meier, and B. Wolff. Generic interfaces for transformation systems and interactive theorem provers. In B. Buth K.Berghammer, J.Peleska, editor, Proceedings of the “International Workshop for Tool Support in Verification and Validation'', BISS Monographs. Shaker Verlag, 1997. [ bib | .ps.gz ]

1996

• C. Lüth, S. Westmeier, and B. Wolff. sml_tk: Functional programming for graphical user interfaces. Technical Report 8/96, Universität Bremen, 1996. [ bib | .ps.gz ]
• Kolyang, C. Lüth, T. Meier, and B. Wolff. Generating graphical user-interfaces in a functional setting. In N. Merriam, editor, Proceedings of the User Interfaces for Theorem Provers (UITP 96), Technical Report. University of York, 1996. [ bib | .ps.gz ]
• Kolyang, T. Santen, and B. Wolff. Correct and user-friendly implementation of transformation systems. In M.-C. Gaudel and J. Woodcock, editors, FME 96 - Industrial Benefits and Advances in Formal Methods, LNCS 1051, pages 629-648. Springer Verlag, 1996. [ bib | DOI | pdf | .ps.gz | Abstract ]
• Kolyang, T. Santen, and B. Wolff. A structure preserving encoding of z in isabelle/hol. In J. von Wright, J. Grundy, and J. Harrison, editors, Theorem Proving in Higher Order Logics - 9th International Conference, LNCS 1125, pages 283-298. Springer Verlag, 1996. [ bib | pdf | .ps.gz | Abstract ]
• M.-C. Gaudel, P. Dauchy, and C. Khoury. A formal specification of the steam-boiler control problem by algebraic specifications with implicit state. In Formal Methods for Industrial Applications: specifying and programming the Steam Boiler Control, volume 1165 of Lecture Notes in Computer Science, pages 233-264. Springer-Verlag, 1996. [ bib | pdf ]

1995

• A. Arnold, M. Gaudel, and B. Marre. An experiment on the validation of a specification by heterogeneous formal means: The transit node. In 5th IFIP Working Conference on Dependable Computing for Critical Applications (DCCA5), pages 24-34, 1995. [ bib ]
• B. Krieg-Brückner, J. Liu, H. Shi, and B. Wolff. Towards correct, efficient and re-usable transformational developments. In M. Broy and S. Jähnichen, editors, KORSO - Methods, Languages, and Tools for the Construction of Correct Software, LNCS 1009, pages 270-284. Springer Verlag, 1995. [ bib | .ps.gz ]
• M.-C. Gaudel. Testing can be formal, too. In TAPSOFT'95, International Joint Conference, Theory And Practice of Software Development, volume 915 of Lecture Notes in Computer Science, pages 82-96, Aarhus, Denmark, 1995. Springer Verlag. [ bib | pdf ]
• Kolyang and B. Wolff. Development by refinement revisited: Lessons learnt from an example. In G. Snelting, editor, Beiträge der GI-Fachtagung “Softwaretechnik 95'', Braunschweig, Mitteilungen der Fachgruppen `Software Engineering' und `Requirements-Engineering',Band 15, Heft 3, ISSN 0720-8928, pages 57-66. GI, 1995. [ bib | .ps.gz ]

1993

• P. Dauchy, M.-C. Gaudel, and B. Marre. Using algebraic specifications in software testing : a case study on the software of an automatic subway. Journal of Systems and Software, 21(3):229-244, 1993. [ bib | pdf ]

1992

• G. Bernot, M.-C. Gaudel, and B. Marre. A formal approach to software testing. In 2nd International Conference on Algebraic Methodology and Software Technology (AMAST), number 670 in Worshops in Computing Series, pages 243-253. Springer Verlag, 1992. [ bib | pdf ]

1991

• G. Bernot, M.-C. Gaudel, and B. Marre. Software testing based on formal specifications: a theory and a tool. Software Engineering Journal, 6(6):387-405, 1991. [ bib | pdf ]

1986

• L. Bougé, N.Choquet, L. Fribourg, and M.-C. Gaudel. Test set generation from algebraic specifications using logic programming. Journal of Systems and Software, 6(4):343-360, 1986. [ bib ]