Filters
+2015
2014
Delphine Longuet, Frédéric Tuong and Burkhart Wolff. Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection. In Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014.. 2014, 43–52.
[ BibTeX ]Achim D Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente and Burkhart Wolff. Panel Discussion: Proposals for Improving OCL. In Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014.. 2014, 83–99.
[ BibTeX ]Achim D Brucker, Lukas Brügger and Burkhart Wolff. The Unified Policy Framework (UPF). Archive of Formal Proofs, 2014. \urlhttp://afp.sf.net/entries/UPF.shtml, Formal proof development.
[ BibTeX ]Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Julien Schmaltz. Formal Specification of a Generic Separation Kernel. Archive of Formal Proofs, 2014. \urlhttp://afp.sf.net/entries/CISC-Kernel.shtml, Formal proof development.
[ BibTeX ]Fatiha Zaidi Huu Nghia Nguyen and Ana Cavalli. A framework for distributed Testing of Timed Composite Systems. In The 21st Asia-Pacific Software Engineering Conference, APSEC 2014. December 2014.
[ BibTeX ]
2013
Thierry Jéron, Margus Veanes and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). Dagstuhl Reports 3(1):1–29, 2013.
[ BibTeX ]Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel and Burkhart Wolff. The Circus Testing Theory Revisited in Isabelle/HOL. In Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods(ICFEM). Series Lecture Notes in Computer Science, number 8144, Springer-Verlag, 2013.
[ BibTeX | pdf ]Achim D Brucker, Lukas Brügger and Burkhart Wolff. HOL-TestGen/FW: An Environment for Specification-based Firewall Conformance Testing. In International Colloquium on Theoretical Aspects of Computing (ICTAC). Series Lecture Notes in Computer Science, number 8049, Springer-Verlag, 2013.
[ BibTeX | pdf ]Burkhart Wolff, Marie-Claude Gaudel and Abderrahmane Feliachi (eds.). Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers LNCS 7681. Springer, 2013.
[ BibTeX ]Achim D Brucker, Delphine Longuet, Frédéric Tuong and Burkhart Wolff. On the Semantics of Object-Oriented Data Structures and Path Expressions. In OCL@MoDELS 1092. 2013, 23-32.
[ BibTeX ]Achim D Brucker, Dan Chiorean, Tony Clark, Birgit Demuth, Martin Gogolla, Dimitri Plotnikov, Bernhard Rumpe, Edward D Willink and Burkhart Wolff. Report on the Aachen OCL Meeting. In OCL@MoDELS 1092. 2013, 103-111.
[ BibTeX ]Burkhart Wolff, Marie-Claude Gaudel and Abderrahmane Feliachi (eds.). Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers 7681. Springer, 2013.
[ BibTeX ]Marie-Claude Gaudel, Richard Lassaigne, Frédéric Magniez and Michel Rougemont. Some approximations in Model Checking and Testing. CoRR abs/1304.5199, 2013.
[ BibTeX ]Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaïdi. Invariants for finite instances and beyond. In Formal Methods in Computer-Aided DEsign, FMCAD. October 2013, 61-68.
[ BibTeX ]Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. Automatic skeleton generation for data-aware service choreographies. In IEEE 24th International Symposium on Software Reliability Engineerinf, ISSRE 2013. November 2013, 320-329.
[ BibTeX ]Romain Aissat and Jean-Yves Pierron. Méthode de validation par génération alétoire de chemins dans des modèles à base d'automates communicants. In Approches Formelles dans l'Assistance au Développement de Logiciels. 2013, 33 – 47.
[ BibTeX ]
2012
Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel. Isabelle/Circus. Archive of Formal Proofs, 2012. \urlhttp://afp.sourceforge.net/entries/Circus.shtml, Formal proof development.
[ BibTeX ]Abderrahmane Feliachi. Semantics-Based Testing for Circus. Phd Thesis, Université Paris Sud, December 2012. Directeurs: Prof. Marie-Claude Gaudel and Prof. Burkhart Wolff.
[ BibTeX ]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. STTT, International Journal on Software Tools for Technology Transfer 14(1):73-93, 2012.
[ BibTeX | pdf ]Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaïdi. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems. In 24th International Conference, CAV 2012 7358. July 2012, 718–724.
[ BibTeX ]Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. Online Verification of Value-Passing Choreographies through Property-Oriented Passive Testing. In IEEE (ed.). 14th IEEE International High Assurance Systems Engineering Symposium (HASE 12). November 2012, 106-113.
[ BibTeX ]Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. In International Conference on Service Oriented Computing (ICSOC 12). 2012, 525–532.
[ BibTeX ]Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. Passive Conformance Testing of Service Choreographies. In ACM (ed.). 27th ACM Symposium on Applied Computing (SAC 2012). March 2012, 1528-1535.
[ BibTeX ]Johan Jeuring, John A Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel and Volker Sorge (eds.). Intelligent Computer Mathematics –- 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings 7362. Springer, 2012.
[ BibTeX ]Makarius Wenzel. Isabelle/jEdit –- A Prover IDE within the PIDE Framework. In Johan Jeuring al (ed.). Intelligent Computer Mathematics –- 11th International Conference (CICM/MKM 2012) 7362. 2012.
[ BibTeX ]
2011
Jordi Cabot, Robert Clarisó, Martin Gogolla and Burkhart Wolff. Preface (OCL 2011 Proceedings). ECEASST 44, 2011.
[ BibTeX ]Burkhart Wolff and Fatiha Za\"\idi (eds.). Testing Software and Systems - 23rd IFIP WG 6.1 International Conference, ICTSS 2011, Paris, France, November 7-10, 2011. Proceedings 7019. Springer, 2011.
[ BibTeX ]Martin Gogolla and Burkhart Wolff (eds.). Tests and Proofs - 5th International Conference, TAP 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings 6706. Springer, 2011.
[ BibTeX ]Ana Cavalcanti, Marie-Claude Gaudel, Robert Hierons and Manuel Nunez. Conformance Relations for Distributed Testing based on CSP. In Fatiha Zaidi and Burkhart Wolff (eds.). Testing Software and Systems, ICTSS 2011 proceedings 7019. 2011, 48-63.
[ BibTeX ]Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne and Sylvain Peyronnet. Uniform Monte-Carlo model checking. In Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 6603. 2011, 127-140.
[ BibTeX | pdf ]Mazen El Maarabani, Ana Cavalli, Iksoon Hwang and Fatiha Zaidi. Verification of Interoperability Security Policies By Model Checking. In IEEE (ed.). High Assurance Systems Engineering (HASE). November 2011, 1-7.
[ BibTeX ]Poizat P L. Bentakouk and F Zaidi. Checking the Behavioral Conformance of Web services with Symbolic Testing and an SMT Solver. In Springer (ed.). Tests & Proofs, TAP 6706. July 2011, 33–50.
[ BibTeX ]Carneiro A Viana, S Maag and F Zaïdi. One step forward: Linking Wireless Self-Organising Networks Validation Techniques with Formal Testing approaches. ACM Computing Survey 43(2):1–39, January 2011.
[ BibTeX ]Makarius Wenzel and Burkhart Wolff. Isabelle/PIDE as Platform for Educational Tools. In Pedro Quaresma and Ralph-Johan Back (eds.). Proceedings First Workshop on CTP Components for Educational Software (THedu'11) 79. 2011.
[ BibTeX ]M Wenzel. Isabelle as Document-oriented Proof Assistant. In James H Davenport, William M Farmer, Florian Rabe and Josef Urban (eds.). Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011) 6824. 2011.
[ BibTeX ]Matthias P Krieger and Achim D Brucker. Extending OCL Operation Contracts with Objective Functions. ECEASST 44, 2011. Proceedings of the International Workshop on OCL and Textual Modelling (OCL 2011).
[ BibTeX ]Matthias P Krieger. Test Generation and Animation Based on Object-Oriented Specifications. Phd Thesis, Université Paris-Sud, 2011.
[ BibTeX ]Paulo Salem Silva. Multi-Agent Systems Verification by Means of Simulation Analysis. Phd Thesis, Université Paris Sud, November 2011. Directeur: Prof. Marie-Claude Gaudel, co-tutelle avec l'Université de Sao Paulo.
[ BibTeX ]Pascal Poizat. Formal Model-Based Approaches for the Development of Composite Systems. HDR, Université Paris Sud, December 2011. Examinateurs: Prof. Philippe Dague, Prof. Marie-Claude Gaudel, Prof. Ernesto Pimentel.
[ BibTeX ]Matthias Krieger. Test Generation and Animation Based on Object-Oriented Specifications. Phd Thesis, Université Paris Sud, 2011. Directeur de thése: Prof. Burkhart Wolff.
[ BibTeX ]Lina Bentakouk. Test symbolique de services Web composite. Phd Thesis, Université Paris Sud, 2011. Directeur de thése: Dr. Fatiha Zaidi, Dr. Pascal Poizat.
[ BibTeX ]Paulo Salem Silva and Ana C V Melo. On-The-Fly Verification of Discrete Event Simulations by Means of Simulation Purposes. In Proceedings of the 2011 Spring Simulation Multiconference (SpringSim'11). 2011.
[ BibTeX ]Paulo Salem Silva and Ana C V Melo. A Formal Environment Model for Multi-Agent Systems. In Jim Davies, Leila Silva and Adenilso Simao (eds.). Formal Methods: Foundations and Applications. Series Lecture Notes in Computer Science, volume 6527, Springer Berlin / Heidelberg, 2011, pages 64-79.
[ BibTeX ]
2010
Abderrahmane Feliachi. Tests generation from Circus specifications. In MOdelling and VErifying parallel Processes (MOVEP). June 2010, 70–75.
[ BibTeX ]Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel and Jim Woodcock (eds.). Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings 6255. Springer, 2010.
[ BibTeX ]Johan Oudinet, Alain Denise and Marie-Claude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. In Conference on random and exhaustive generation of combinatorial objects (GASCom). September 2010. 10 pages.
[ BibTeX ]Marie-Claude Gaudel. Software Testing Based on Formal Specification. In Paulo Borba, Ana Cavalcanti, Augusto Sampaio and Jim Woodcock (eds.). Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, PSSE 2007, December 3-7, 2007, Revised Lectures 6153. 2010, 215-242.
[ BibTeX ]Fatiha Zaidi, Mounir Lallali and Stephane Maag. A Component based Testing Technique for a Manet Routing Protocol. In AICCSA'2010 - ACS/IEEE International Conference on Computer Sustems and Applications. May 2010, 1–7.
[ BibTeX ]A Cavalli, T-D Cao, W Mallouli, E Martins, A Sadovykh, S Salva and F Zaidi. WebMov : A Dedicated Framework for the Modelling and Testing of Web Services. In ICWS 2010 - IEEE International Conference on Web Services. July 2010, 377–384.
[ BibTeX ]A Carneiro, T Herault, T Largillier, S Peyronnet and F Zaidi. Supple: A Flexible Probabilistic Data Dissemination Protocol for Wireless Sensor Networks. In MSWIM'2010 - The 13th ACM International Conference on Modeling Analysis and Simulation of Wireless and Mobile Systems. October 2010, 385–393.
[ BibTeX ]A Cavalli, M Lallali, S Maag, G Morales and F Zaidi. Emergent Web Intelligence. Series Advanced Information and Knowledge Processing, chapter Modeling and Testing of Web Based Systems: Advanced Semantic Technologies, pages 355–392, Springer Verlag, 2010.
[ BibTeX ]D Matthews and M Wenzel. Efficient Parallel Programming in Poly/ML and Isabelle/ML. In ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010). 2010.
[ BibTeX ]Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In Sacerdoti C Coen and D Aspinall (eds.). User Interfaces for Theorem Provers (UITP 2010). July 2010. FLOC 2010 Satellite Workshop.
[ BibTeX ]Johan Oudinet. Approches combinatoires pour le test statistique a grande échelle. Phd Thesis, Université Paris Sud, November 2010. Directeur: Prof. Marie-Claude Gaudel.
[ BibTeX ]
2009
Achim D Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Marsha Chechik and Martin Wirsing (eds.). Fundamental Approaches to Software Engineering (FASE09). Series Lecture Notes in Computer Science, number 5503, Springer-Verlag, 2009, pages 417–420.
[ BibTeX | 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 5826. November 2009, 16–32.
[ BibTeX ]F Zaïdi, A Cavalli and E Bayse. NetworkProtocol Interoperability Testing based on Contextual. In 24th Annual ACM Symposium on Applied on Applied Computing. March 2009, 2–7.
[ BibTeX ]A Cavalli, S Maag, Montes E 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. March 2009, 1–6.
[ BibTeX ]Florian Haftmann and Makarius Wenzel. Local theory specifications in Isabelle/Isar. In Stefano Berardi, Ferruccio Damiani and Ugo Liguoro (eds.). Types for Proofs and Programs, TYPES 2008 5497. 2009.
[ BibTeX ]Norbert Schirmer and Makarius Wenzel. State Spaces –- The Locale Way. In Ralf Huuck, Gerwin Klein and Bastian Schlich (eds.). Systems Software Verification (SSV 2009). 2009.
[ BibTeX ]M Wenzel. Parallel Proof Checking in Isabelle/Isar. In G Dos Reis and L Théry (eds.). ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). 2009.
[ BibTeX ]Paulo Salem Silva. An Environment Specification Language for Multi-Agent Systems. 2009. Technical Report 1531 – Universit Paris-Sud 11, Laboratoire de Recherche en Informatique.
[ BibTeX ]
2008
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 (eds.). 21th International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2008). Series LNCS 5170, Springer-Verlag, 2008.
[ BibTeX | pdf ]Ana Cavalcanti and Marie-Claude Gaudel. A note on traces refinement and the {\textitconf} relation in the Unifying Theories of Programming. In Andrew Butterfield (ed.). Unifying Theories of Programming, Second International Symposium, UTP 2008, Trinity College, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers 5713. 2008, 42–61.
[ BibTeX | pdf ]Stefan Berghofer and Makarius Wenzel. Logic-free reasoning in Isabelle/Isar. In Intelligent Computer Mathematics –- Mathematical Knowledge Management (MKM 2008) 5144. 2008.
[ BibTeX ]M Wenzel, L C Paulson and T Nipkow. The Isabelle Framework. In Theorem Proving in Higher Order Logics (TPHOLs 2008). 2008. Invited paper.
[ BibTeX ]Johan Oudinet. Uniform Random Exploration of Concurrent Systems. In MOdelling and VErifying parallel Processes (MOVEP). June 2008, 323–328.
[ BibTeX ]J Fayolle, M -C Gaudel, S -D Gouraud and B Marre. Statistical Testing of Synchronous Reactive Systems. In ERTS. 2008.
[ BibTeX ]
2007
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.
[ BibTeX | pdf ]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..
[ BibTeX ]F Zaidi and Mounir Lallali. Use of Verification Techniques for Components Testing. Number 1465, LRI, http://www.lri.fr/Rapports-internes, January 2007.
[ BibTeX ]M Lallali, F Zaidi and A Cavalli. Timed Modeling of Web Services Composition for Automatic Testing. Number 07008-LOR, GET/INT, September 2007. Long version.
[ BibTeX ]Amine Chaieb and Makarius Wenzel. Context aware Calculation and Deduction –- Ring Equalities via Gröbner Bases in Isabelle. In Manuel Kauers, Manfred Kerber, Robert Miner and Wolfgang Windsteiger (eds.). Towards Mechanized Mathematical Assistants (CALCULEMUS 2007) 4573. 2007.
[ BibTeX ]Florian Haftmann and Makarius Wenzel. Constructive Type Classes in Isabelle. In T Altenkirch and C McBride (eds.). Types for Proofs and Programs (TYPES 2006) 4502. 2007.
[ BibTeX ]Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded into Isabelle/Isar. In Jacques Carette and Freek Wiedijk (eds.). Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007). Hagenberg, Austria. June 2007.
[ BibTeX ]M Wenzel and B Wolff. Building Formal Method Tools in the Isabelle/Isar Framework. In K Schneider and J Brandt (eds.). Theorem Proving in Higher Order Logics (TPHOLs 2007) 4732. 2007.
[ BibTeX ]Makarius Wenzel. Isabelle/Isar –- a generic framework for human-readable proof documents. In R Matuszewski and A Zalewska (eds.). From Insight to Proof –- Festschrift in Honour of Andrzej Trybulec. Series Studies in Logic, Grammar, and Rhetoric, volume 10(23), University of Białystok, 2007.
[ BibTeX ]
2006
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 (eds.). MoDELS 2006: Model Driven Engineering Languages and Systems. Series LNCS 4199, Springer-Verlag, 2006, pages 306–320. An extended version of this paper is available as ETH Technical Report, no. 524..
[ BibTeX | pdf ]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 (eds.). International Workshop on Software Verification and Validation (SVV 2006). Series Computing Research Repository (CoRR), 2006.
[ BibTeX | pdf ]Manuel Núñez Garc\'\ia, Klaus Havelund, Grigore Rosu and Burkhart Wolff (eds.). Proceedings of the International Workshop on Formal Aspects of Testing and Runtime Verification (FATES/RV). Springer Verlag, Seattle, USA, 2006. LNCS 4262..
[ BibTeX ]M -C Gaudel. Validation et Vérification. In Encyclopédie de l'informatique et des systèmes d'information. Vuibert, 2006, pages 1136-1150.
[ BibTeX ]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.
[ BibTeX ]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). October 2006.
[ BibTeX ]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. 2006, 48–55. http://doi.acm.org/10.1145/1163653.1163663.
[ BibTeX | pdf ]S Maag and F Zaidi. Spécification Formelle pour le Test d'un Protocole de Routage ad hoc. Number 06009-LOR, GET/INT, October 2006.
[ BibTeX ]Markus Wenzel and Lawrence C Paulson. Isabelle/Isar. In F Wiedijk (ed.). The Seventeen Provers of the World. Series LNAI, volume 3600, Springer, 2006.
[ BibTeX ]Makarius Wenzel. Structured Induction Proofs in Isabelle/Isar. In J Borwein and W Farmer (eds.). Mathematical Knowledge Management (MKM 2006) 4108. 2006.
[ BibTeX ]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). 2006, 10-19.
[ BibTeX ]
2005
Achim D Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 User Guide. Number 482, Computer Security Group, ETH Zürich, April 2005.
[ BibTeX ]Achim D Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Wolfgang Grieskamp and Carsten Weise (eds.). Formal Approaches to Testing of Software (FATES 05). Series LNCS 3997, Springer-Verlag, 2005, pages 87–102.
[ BibTeX ]Achim D Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Jens Grabowski and Brian Nielsen (eds.). Formal Approaches to Testing of Software (FATES 04). Series LNCS 3395, Springer-Verlag, 2005, pages 16–32.
[ BibTeX ]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.
[ BibTeX ]
2004
Achim D Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. Number 449, Computer Security Group, ETH Zürich, June 2004.
[ BibTeX ]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. August 2004, 165-174.
[ BibTeX ]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.
[ BibTeX ]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 (eds.). Testing of Communicating Systems (Testcom'04). March 2004, 17–19.
[ BibTeX ]S -D Gouraud. AuGuSTe: un outil pour le Test Statistique. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). 2004, 337-340.
[ BibTeX ]A Denise, M -C Gaudel and S -D Gouraud. A Generic Method For Statistical Testing. Number 1386, 2004.
[ BibTeX ]
2003
David Basin and Burkhart Wolff (eds.). Theorem Proving in Higher Order Logics, 16th International Conference (TPHOLs 2003). Springer-Verlag, Rome, Italy, September 2003. LNCS 2758..
[ BibTeX ]Achim D Brucker and Burkhart Wolff. Using Theory Morphisms for Implementing Formal Methods Tools. In Herman Geuvers and Freek Wiedijk (eds.). Types 2002, Proceedings of the workshop Types for Proof and Programs. Series LNCS 2646, Springer-Verlag, 2003.
[ BibTeX ]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. October 2003.
[ BibTeX ]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. October 2003.
[ BibTeX ]A Mederreg, F Zaïdi, P Combes, W Monin, R Castanet, M MacKaya and P Lauren\~cot. Une Plate-forme de Validation Multi-Services et Multi-Protocoles - Résultats d'Expérimentations. In Riguidel Serhouchni M A A. Cavalli (ed.). CFIP'2003 Ingénierie des Protocoles. October 2003, 135–151.
[ BibTeX ]Fatiha Zaïdi. Platonis - rapport final. Delivrable, Institut National des Télécommunications, France, 2003.
[ BibTeX ]
2002
A Cavalli, A Mederreg and F Zaïdi. Mobiles Services Validation. In Nagib Callaos and al (eds.). The 6th World Conference on Systemics, Cybernics and Informatics. July 2002.
[ BibTeX ]Cédric Besse, Ana R Cavalli, Myungchul Kim and Fatiha Za\"\idi. Automated Generation of Interoperability Tests. In FIP/TC6/WG6.1 Fourteenth International Conference on Testing of Communicating Systems (Testcom 2002). March 2002, 169-184. ISBN 0-7923-7695-1.
[ BibTeX ]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.
[ BibTeX ]Tobias Nipkow, Lawrence C Paulson and Markus Wenzel. Isabelle/HOL –- A Proof Assistant for Higher-Order Logic. Series LNCS, volume 2283, Springer, 2002.
[ BibTeX ]Markus Wenzel. Isabelle/Isar –- a versatile environment for human-readable formal proof documents. Phd Thesis, Institut für Informatik, TU München, 2002.
[ BibTeX ]Freek Wiedijk and Markus Wenzel. A comparison of the mathematical proof languages Mizar and Isar.. Journal of Automated Reasoning 29(3-4), 2002.
[ BibTeX ]
2001
Burkhart Wolff. Verifying Explicit Substitution Calculi in Binding Structures with Effect Binding. In Pierre Lescanne (ed.). Workshop on Explicit Substitution Theory and Applications (WESTAPP'01) 210. May 2001, 58 – 71.
[ BibTeX ]Marie-Claude Gaudel. Testing from Formal Specifications, a Generic Approach. In Dirk Craeynest and Alfred Strohmeier (eds.). Reliable SoftwareTechnologies Ada-Europe 2001 2043. 2001, 35-48. invited lecture.
[ BibTeX ]A Cavalli, B Defude, Ch. Rinderknecht and F Zaïdi. A Service-Component Testing Method adn Suitable CORBA Architecture. In IEEE Computer Society (ed.). Proceedings of the Sixth IEEE Symposium on Computers and Communications. July 2001, 655–660.
[ BibTeX ]Fatiha Zaïdi. Contribution a la génération de tests pour les composants de service. Application aux services de Réseau Intelligent. Phd Thesis, Université d'Evry, 2001.
[ BibTeX ]F Zaïdi. Open Problems in protocol testing. Workshop on protocol and dsitributed systems testing, October 2001.
[ BibTeX ]Fatiha Zaïdi. Test du Service RPVM. Delivrable FC-T222, Institut National des Télécommunications, France, 2001.
[ BibTeX ]Gertrud Bauer and Markus Wenzel. Calculational reasoning revisited –- an Isabelle/Isar experience. In R J Boulton and P B Jackson (eds.). Theorem Proving in Higher Order Logics (TPHOLs 2001) 2152. 2001.
[ BibTeX ]S -D Gouraud, A Denise, M -C Gaudel and B Marre. A New Way of Automating Statistical Testing Methods. Number 1290, 2001.
[ BibTeX ]
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 (ed.). CFIP'2000 Ingénierie des protocoles. October 2000, 363-378.
[ BibTeX ]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.
[ BibTeX ]Gertrud Bauer and Markus Wenzel. Computer-Assisted Mathematics at Work –- The Hahn-Banach Theorem in Isabelle/Isar. In Thierry Coquand, Peter Dybjer, Bengt Nordström and Jan Smith (eds.). Types for Proofs and Programs (TYPES 1999) 1956. 2000.
[ BibTeX ]
1999
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.
[ BibTeX ]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. (eds.). Proceeding of IFIP International conference FORTE/PSTV'99. October 1999, 41-56.
[ BibTeX ]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. November 1999, 22-24.
[ BibTeX ]Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL –- lessons learned in Formal-Logic Engineering. In Y Bertot, G Dowek, A Hirschowitz, C Paulin and L Thery (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1999) 1690. 1999.
[ BibTeX ]Florian Kammüller, Markus Wenzel and Lawrence C Paulson. Locales: A Sectioning Concept for Isabelle. In Y Bertot, G Dowek, A Hirschowitz, C Paulin and L Thery (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1999) 1690. 1999.
[ BibTeX ]Markus Wenzel. Isar –- a Generic Interpretative Approach to Readable Formal Proof Documents. In Y Bertot, G Dowek, A Hirschowitz, C Paulin and L Thery (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1999) 1690. 1999.
[ BibTeX ]
1998
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 (ed.). 11. International Conference of Z Users ZUM'98. 1998, 116–134.
[ BibTeX ]C Lüth, E W Karlsen, Kolyang, S Westmeier and B Wolff. Tool integration in the UniForM Workbench. In Berghammer and Hoffmann (eds.). Workshop on Tool Support for System Specification, Development, and Verification. 1998.
[ BibTeX ]Wolfgang Naraschewski and Markus Wenzel. Object-Oriented Verification based on Record Subtyping in Higher-Order Logic. In Jim Grundy and Malcom Newey (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1998) 1479. 1998.
[ BibTeX ]
1997
Kolyang, C Lüth, T Meier and B Wolff. TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving. In Dauchet M M. Bidoit (ed.). TAPSOFT 97: Theory and Practice of Software Development. 1997, 855–858.
[ BibTeX ]Kolyang, C L\"uth, T Meier and B Wolff. Generic Interfaces for Transformation Systems and Interactive Theorem Provers.. In Buth B K.Berghammer J.Peleska (ed.). Proceedings of the “International Workshop for Tool Support in Verification and Validation{\'}{\'}. 1997.
[ BibTeX ]B Wolff. A Generic Calculus of Transformations. Phd Thesis, Universität Bremen, Aachen, 1997.
[ BibTeX ]M Wenzel. Type Classes and Overloading in Higher-Order Logic. In Elsa L Gunter and Amy Felty (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1997) 1275. 1997.
[ BibTeX ]
1996
Kolyang, C Lüth, T Meier and B Wolff. Generating Graphical User-Interfaces in a Functional Setting. In N Merriam (ed.). Proceedings of the User Interfaces for Theorem Provers (UITP 96). 1996.
[ BibTeX ]C Lüth, S Westmeier and B Wolff. sml_tk: Functional Programming for Graphical User Interfaces. Number 8/96, Universität Bremen, 1996.
[ BibTeX ]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. Series Lecture Notes in Computer Science, volume 1165, Springer-Verlag, 1996, pages 233-264.
[ BibTeX | pdf ]
1995
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 (eds.). KORSO –- Methods, Languages, and Tools for the Construction of Correct Software. 1995, 270–284.
[ BibTeX ]Kolyang and B Wolff. Development by Refinement Revisited: Lessons learnt from an example.. In G Snelting (ed.). Beiträge der GI-Fachtagung “Softwaretechnik 95{\'}{\'}, Braunschweig. 1995, 57–66.
[ BibTeX ]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). 1995, 24–34.
[ BibTeX ]
1993
1992
1991
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.
[ BibTeX ]