2011

2011.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2011.bib -c 'year = 2011' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@article{RASTA:STTT:2011,
  author = {Alain Denise and Marie-Claude Gaudel and Sandrine-Dominique Gouraud and Richard Lassaigne and Johan Oudinet and Sylvain Peyronnet },
  title = {Coverage-Biased Random Exploration of Large Models and Application to Testing},
  journal = {STTT, International Journal on Software Tools for Technology Transfer},
  year = {2011},
  volume = {accepted},
  note = {26 pages},
  pdf = {http://www.lri.fr/~bibli/Rapports-internes/2008/RR1494.pdf}
}
@article{CavalGau:Acta:2010,
  author = {Ana Cavalcanti and Marie-Claude Gaudel },
  title = {Testing for Refinement in {C}ircus},
  journal = {Acta Informatica},
  year = {2011},
  volume = {accepted},
  note = {56 pages},
  pdf = {http://www.lri.fr/~mcg/PDF/CavalcantiGaudelCircus221110.pdf}
}
@inproceedings{FASE:2011,
  author = {Johan Oudinet and Alain Denise and Marie-Claude Gaudel and Richard Lassaigne and Sylvain Peyronnet},
  title = {Uniform {M}onte-{C}arlo model checking},
  booktitle = {FASE 2011},
  publisher = {Springer Verlag},
  volume = {to appear},
  series = {Lecture Notes in Computer Science},
  month = {March},
  year = {2011},
  note = {15 pages},
  address = {Saarbrucken},
  pdf = {http://www.lri.fr/~mcg/PDF/FASE.pdf},
  x-equipes = {fortesse},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {A},
  type_digiteo = {conf_isbn}
}

2010

2010.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2010.bib -c 'year = 2010' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@proceedings{ictac2010,
  editor = {Ana Cavalcanti and
               David D{\'e}harbe and
               Marie-Claude Gaudel and
               Jim Woodcock},
  title = {Theoretical Aspects of Computing - ICTAC 2010, 7th International
               Colloquium, Natal, Rio Grande do Norte, Brazil, September
               1-3, 2010. Proceedings},
  booktitle = {ICTAC},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6255},
  year = {2010}
}
@article{acmcs,
  author = {A. Carneiro Viana and S. Maag and F. Za\"idi},
  title = {One step forward: Linking Wireless Self-Organising Networks Validation Techniques with Formal Testing approaches},
  journal = {ACM Computing Survey},
  year = 2010,
  volume = 41,
  number = 3,
  pages = {1--39},
  month = {October},
  note = {In Press. available at http://hal.archives-ouvertes.fr/index.php, HAL: inria-00357655, version 1  }
}
@inproceedings{mswim,
  author = {A. Carneiro and T. Herault and T. Largillier and S. Peyronnet and F. Zaidi},
  title = {Supple: A Flexible Probabilistic Data Dissemination Protocol for Wireless Sensor Networks},
  booktitle = {MSWIM'2010 - The 13th ACM International Conference on Modeling Analysis and Simulation of Wireless and Mobile Systems},
  year = 2010,
  pages = {385--393},
  month = {October},
  address = {Turkey},
  publisher = {ACM}
}
@inbook{livre,
  author = {A. Cavalli and M. Lallali and S. Maag and G. Morales and F. Zaidi},
  title = {Emergent {W}eb {I}ntelligence},
  chapter = {Modeling and Testing of Web Based Systems: Advanced Semantic Technologies},
  publisher = {Springer Verlag},
  year = 2010,
  pages = {355--392},
  series = {Advanced Information and Knowledge Processing}
}
@inproceedings{icws,
  author = {A. Cavalli and T-D. Cao and W. Mallouli and E. Martins and A. Sadovykh and S. Salva and F. Zaidi},
  title = {WebMov : A Dedicated Framework for the Modelling and Testing of Web Services},
  booktitle = {ICWS 2010 - IEEE International Conference on Web Services},
  pages = {377--384},
  year = 2010,
  address = {Miami},
  month = {July}
}
@inproceedings{feliachi10movep,
  author = {Abderrahmane Feliachi},
  title = {Tests generation from Circus specifications},
  booktitle = {MOdelling and VErifying parallel Processes (MOVEP)},
  pages = {70--75},
  year = 2010,
  month = {June},
  x-equipes = {fortesse},
  x-type = {article},
  x-support = {actes}
}
@inproceedings{feliachi10icst,
  author = {Abderrahmane Feliachi and H{\'e}l{\`e}ne LeGuen},
  title = {Generating transition probabilities for automatic model-based test generation},
  booktitle = {International Conference on Software Testing, Verification and Validation {(ICST)}},
  doi = {10.1109/ICST.2010.26},
  pages = {99--102},
  year = 2010,
  month = {April},
  publisher = {IEEE Computer Society},
  address = {Paris, France},
  pdf = {http://www.lri.fr/~feliachi/Papers/ICST10.pdf},
  x-equipes = {fortesse},
  x-type = {article},
  x-support = {actes}
}
@inproceedings{feliachi:uznifying-theories:2010,
  author = {Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff},
  title = {Unifying Theories in Isabelle/HOL},
  booktitle = {Unifying Theories of Programming 2010},
  publisher = {Springer Verlag},
  volume = {to appear},
  series = {Lecture Notes in Computer Science},
  month = {November},
  year = {2010},
  note = {20 pages},
  address = {Shanghai, China},
  pdf = {http://www.lri.fr/~feliachi/Papers/UTP10.pdf},
  x-equipes = {fortesse},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {B},
  type_digiteo = {conf_isbn}
}
@article{brucker.ea:2010,
  author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
  journal = {Software Testing, Verification, and Validation, 2010 International Conference on},
  volume = {0},
  title = {{V}erified {F}irewall {P}olicy {T}ransformations for {T}est {C}ase {G}eneration},
  year = 2010,
  isbn = {978-0-7695-3990-4},
  pages = {345-354},
  publisher = {IEEE Computer Society},
  copyright = {IEEE Computer Society},
  booktitle = {International Conference on Software Testing {(ICST10)}},
  location = {Paris, France},
  editor = {Ana Cavalli and Sudipto Ghosh},
  classification = {conference},
  doi = {10.1109/ICST.2010.50},
  address = {Los Alamitos, CA, USA},
  pdf = {../papers/conf/firewall-reloaded.pdf},
  abstract = {We present an optimization technique for model-based generation of
                   test cases for firewalls. Based on a formal model for firewall
                   policies in higher-order logic, we derive a collection of
                   semantics-preserving policy transformation rules and an algorithm
                   that optimizes the specification with respect of the number of
                   test cases required for path coverage.  The correctness of the rules
                   and the algorithm is established by formal proofs in
                   Isabelle/\acs{hol}. Finally, we use the normalized policies to
                   generate test cases with the domain-specific firewall testing tool
                   \testgenFW.
 
                   The resulting procedure is characterized by a gain in efficiency
                   of two orders of magnitude and can handle configurations with
                   hundreds of rules as occur in practice.
                  
                   Our approach can be seen as an instance of a methodology to
                   tame inherent state-space explosions in test case generation for
                   security policies.}
}
@techreport{brucker.ea:hol-testgen:2010,
  author = {Achim D. Brucker and Lukas Br{\"u}gger and Matthias P.
		  Krieger and Burkhart Wolff},
  institution = {ETH Zurich},
  language = {USenglish},
  month = {April},
  number = 670,
  pdf = {http://www.lri.fr/~wolff/papers/other/HOL-TestGen_UserGuide.pdf},
  title = {{HOL-TestGen} 1.5.0 User Guide},
  url = {http://www.lri.fr/~wolff/papers/other/HOL-TestGen_UserGuide.pdf
		  },
  year = 2010
}
@article{AL10,
  author = {Aiguier, Marc and Longuet, Delphine},
  title = {Some general results about proof normalization},
  journal = {Logica Universalis},
  volume = {4},
  number = {1},
  pages = {1-29},
  year = {2010},
  abstract = {In this paper, we provide a general setting under which results of
normalization of proof trees such as, for instance, the logicality result in
equational reasoning and the cut-elimination property in sequent or natural
deduction calculi, can be unified and generalized. This is achieved by giving
simple conditions which are sufficient to ensure that such normalization
results hold, and which can be automatically checked since they are
syntactical. These conditions are based on basic properties of elementary
combinations of inference rules which ensure that the induced global proof
tree transformation processes do terminate.},
  pdf = {http://www.lri.fr/~longuet/Publications/AL10-LU.pdf}
}
@inproceedings{CavalGau:UTP:2010,
  author = {Ana Cavalcanti and Marie-Claude Gaudel},
  title = {Specification coverage for testing in {C}ircus},
  booktitle = {Unifying Theories of Programming 2010},
  publisher = {Springer Verlag},
  volume = {to appear},
  series = {Lecture Notes in Computer Science},
  month = {November},
  year = {2010},
  note = {45 pages},
  address = {Shanghai, China},
  pdf = {http://www.lri.fr/~mcg/PDF/CavalcantiGaudelUTP-2.pdf},
  x-equipes = {fortesse},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {B},
  type_digiteo = {conf_isbn}
}
@inproceedings{Brucker.ea:SpecificationBased:2010,
  author = {Brucker, Achim D. and Krieger, Matthias P. and Longuet, Delphine and Wolff, Burkhart},
  title = {A Specification-based Test Case Generation Method for {UML/OCL}},
  booktitle = {Workshop on OCL and Textual Modelling},
  year = {2010},
  note = {Selected as best paper, to appear in LNCS},
  abstract = {Automated test data generation is an important method for the verification and validation of \UML/\OCL specifications. In this paper, we present an extension of \DNF-based test case generation methods to class models and recursive query operations on them. A key feature of our approach is an implicit representation of object graphs avoiding a representation based on object-id's; thus, our approach avoids the generation of isomorphic object graphs by using a concise and still human-readable symbolic representation.},
  pdf = {http://www.lri.fr/~wolff/papers/workshop/ocl-testing.pdf}
}
@inproceedings{Matthews-Wenzel:2010,
  author = {D. Matthews and M. Wenzel},
  title = {Efficient Parallel Programming in {Poly/ML} and {Isabelle/ML}},
  booktitle = {ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010)},
  year = 2010,
  url = {http://www.lri.fr/~wenzel/papers/parallel-ml.pdf}
}
@inproceedings{aiccsa,
  author = {Fatiha Zaidi and Mounir Lallali and Stephane Maag},
  title = {A Component based Testing Technique for a Manet Routing Protocol},
  booktitle = {AICCSA'2010 - ACS/IEEE International Conference on Computer Sustems and Applications},
  pages = {1--7},
  year = 2010,
  month = {May}
}
@inproceedings{gascom10,
  author = {Johan Oudinet and Alain Denise and Marie-Claude Gaudel},
  title = {A new dichotomic algorithm for the uniform random generation of words in regular languages},
  booktitle = {Conference on random and exhaustive generation of combinatorial objects ({GASCom})},
  year = 2010,
  address = {Montreal, Canada},
  month = {September},
  note = {10 pages},
  publisher = {To appear}
}
@article{LAL09,
  author = {Longuet, Delphine and Aiguier, Marc and Le Gall, Pascale},
  title = {Proof-guided test selection from quantifier-free first-order specifications with equality},
  journal = {Journal of Automated Reasoning, special issue on Tests and Proofs},
  year = {2010},
  volume = {45},
  number = {4},
  pages = {437-473},
  abstract = {This paper deals with test case selection from axiomatic specifications whose axioms are quantifier-free first-order formulas with equality. We first prove the existence of an ideal exhaustive test set to start the selection from. We then propose an extension of the test selection method called axiom unfolding, originally defined for algebraic specifications, to quantifier-free first-order specifications with equality. This method basically consists of a case analysis of the property under test (the test purpose) according to the specification axioms. It is based on a proof search for the different instances of the test purpose. Since the calculus is sound and complete, this allows us to provide a full coverage of this property. The generalisation we propose allows to deal with any kind of predicate (not only equality) and with any form of axiom and test purpose (not only equations or Horn clauses). Moreover, it improves our previous works with efficiently dealing with the equality predicate, thanks to the paramodulation rule.},
  pdf = {http://www.lri.fr/~longuet/Publications/LAL10-JAR.pdf}
}
@inproceedings{Wenzel:2010,
  author = {Makarius Wenzel},
  title = {Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}},
  booktitle = {User Interfaces for Theorem Provers (UITP 2010), FLOC 2010 Satellite Workshop},
  year = 2010,
  editor = {C. Sacerdoti Coen and D. Aspinall},
  series = {ENTCS},
  month = {July},
  publisher = {Elsevier},
  url = {http://www.lri.fr/~wenzel/papers/async-isabelle-scala.pdf}
}
@inproceedings{Gaudel07,
  author = {Marie-Claude Gaudel},
  title = {Software Testing Based on Formal Specification},
  booktitle = {Testing Techniques in Software Engineering, Second Pernambuco
               Summer School on Software Engineering, PSSE 2007, December 3-7, 2007, Revised Lectures},
  pages = {215-242},
  editor = {Paulo Borba and
               Ana Cavalcanti and
               Augusto Sampaio and
               Jim Woodcock},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {6153},
  year = {2010}
}
@inproceedings{Krieger.ea:2010,
  author = {Matthias P. Krieger and Alexander Knapp and Burkhart Wolff},
  title = {{A}utomatic and {E}fficient {S}imulation of {O}peration {C}ontracts},
  booktitle = {Ninth International Conference on Generative Programming and Component Engineering (GPCE'10)},
  year = 2010,
  publisher = {IEEE Computer Society},
  copyright = {IEEE Computer Society},
  editor = {Eelco Visser and Jaakko Jarvi and Giorgios Economopoulos},
  annote = {to appear},
  isbn = {978-1-4503-0154-1},
  doi = {10.1145/1868294.1868303},
  pdf = {../papers/conf/2010-gpce-operation-contracts.pdf},
  abstract = {Operation contracts consisting of pre- and
                  postconditions are a well-known means of specifying
                  operations. In this paper we deal with the problem
                  of operation contract simulation, i.e., determining
                  operation results satisfying the postconditions
                  based on input data supplied by the user; simulating
                  operation contracts is an important technique for
                  requirements validation and prototyping. Current
                  approaches to operation contract simulation exhibit
                  poor performance for large sets of input data or
                  require additional guidance from the user. We show
                  how these problems can be alleviated and describe an
                  efficient as well as fully automatic approach. It is
                  implemented in our tool OCLexec that generates from
                  UML/OCL operation contracts corresponding Java
                  implementations which call a constraint solver at
                  runtime. The generated code can serve as a
                  prototype. A case study demonstrates that our
                  approach can handle problem instances of
                  considerable size.}
}
@inproceedings{PP_PY10,
  author = {Pascal Poizat and Yuhong Yan},
  title = {{Adaptive Composition of Conversational Services through Graph Planning Encoding}},
  booktitle = {Proceedings of the International Symposium On Leveraging Applications of Formal Methods, Verification and Validation (ISoLA 10)},
  optpages = {--},
  year = {2010},
  optvolume = {},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  note = {to appear}
}
@inproceedings{PP_YPZ10c,
  author = {Yuhong Yan and Pascal Poizat and Ludeng Zhao},
  title = {{Repairs vs. Recomposition for Broken Service Compositions}},
  booktitle = {Proceedings of the International Conference on Service Oriented Computing (ICSOC 10)},
  optpages = {--},
  year = {2010},
  optvolume = {},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  note = {to appear}
}
@inproceedings{PP_YPZ10b,
  author = {Yuhong Yan and Pascal Poizat and Ludeng Zhao},
  title = {{Self-Adaptive Service Composition through Graphplan Repair}},
  booktitle = {Proceedings of the International Conference on Web Services (ICWS 10), work-in-progress papers},
  pages = {624--627},
  year = {2010},
  publisher = {IEEE Computer Society}
}
@inproceedings{PP_YPZ10a,
  author = {Yuhong Yan and Pascal Poizat and Ludeng Zhao},
  title = {{Repairing Service Compositions in a Changing World}},
  booktitle = {Selected papers from the 8th ACIS conference on Software Engineering Research, Management & Applications (SERA 10)},
  pages = {17--36},
  year = {2010},
  volume = {296},
  series = {Studies in Computational Intelligence},
  publisher = {Springer}
}

2009

2009.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2009.bib -c 'year = 2009' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{pwm,
  author = {A. Cavalli and S. Maag and E. Montes de Oca and F. Zaidi},
  title = {A Formal Passive Testing Approach to test a MANET Routing Protocol},
  booktitle = {PWN 2009 5th IEEE PerCom Workshop on Pervasive Wireless Networking},
  pages = {1--6},
  year = 2009,
  address = {Texas},
  month = {March},
  publisher = {IEEE}
}
@article{brucker.ea:2009,
  author = {Achim D. Brucker and Burkhart Wolff},
  title = {{S}emantics, {C}alculi, and {A}nalysis for {O}bject-{O}riented {S}pecifications},
  journal = {Acta Informatica},
  volume = 46,
  number = 4,
  pages = {255--284},
  year = 2009,
  abstract = {We present a formal semantics for an object-oriented
                  specification language. The formal semantics is
                  presented as a conservative shallow embedding in
                  Isabelle/HOL and the language is oriented towards
                  OCL formulae in the context of UML class
                  diagrams. On this basis, we formally derive several
                  equational and tableaux calculi, which form the
                  basis of an integrated proof environment including
                  automatic proof support and support for the analysis
                  of this type of specifications.  We show applications
                  of our proof environment to data refinement based on
                  an adapted standard refinement notion. Thus, we
                  provide an integrated formal method for refinement-based 
                  object-oriented development. },
  pdf = {../papers/journals/acta-holocl.pdf},
  keywords = {UML , OCL , object-oriented specification , refinement , formal methods},
  doi = {10.1007/s00236-009-0093-8},
  classification = {journal}
}
@incollection{brucker.ea:hol-testgen:2009,
  title = {{HOL-TestGen:} {A}n {I}nteractive {T}est-case {G}eneration {F}ramework},
  abstract = {We present HOL-TestGen, an extensible test environment for
		  specification-based testing build upon the proof assistant
		  Isabelle. HOL-TestGen leverages the semi-automated
		  generation of test theorems (a form of a partition), and
		  their refinement to concrete test data, as well as the
		  automatic generation of a test driver for the execution and
		  test result verification.
		  
		  HOL-TestGen can also be understood as a unifying technical
		  and conceptual framework for presenting and investigating
		  the variety of unit and sequence test techniques in a
		  logically consistent way. },
  keywords = {symbolic test case generations, black box testing, white
		  box testing, theorem proving, interactive testing},
  location = {York, UK},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Fundamental Approaches to Software Engineering
		  {(FASE09)}},
  language = {USenglish},
  publisher = {Springer-Verlag},
  address = {Heidelberg},
  series = {Lecture Notes in Computer Science},
  number = {5503},
  doi = {10.1007/978-3-642-00593-0_28},
  pages = {417--420},
  editor = {Marsha Chechik and Martin Wirsing},
  categories = {holtestgen},
  classification = {conference},
  year = {2009},
  pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.ps.gz},
  public = {yes},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009}
}
@incollection{brucker.ea:ocl-null:2009,
  author = {Achim D. Brucker and Matthias P. Krieger and Burkhart
                  Wolff},
  booktitle = {MODELS 2009 Workshops},
  series = {LNCS 6002},
  editor = {S. Ghosh},
  pages = {261--275},
  language = {USenglish},
  publisher = {Springer Verlag, Heidelberg},
  title = {Extending {OCL} with Null-References},
  year = 2009,
  classification = {workshop},
  categories = {holocl},
  location = {Denver, Colorado, \acs{usa}},
  areas = {formal methods, software},
  public = {yes},
  abstract = {From its beginnings, OCL is based on a strict semantics
                  for undefinedness, with the exception of the logical
                  connectives of type Boolean that constitute a three-valued
                  propositional logic. Recent versions of the OCL standard
                  added a second exception element, which, similar to the
                  null references in object-oriented programming languages,
                  is given a non-strict semantics. Unfortunately, this
                  extension has been done in an ad hoc manner, which results
                  in several inconsistencies and contradictions.

                  In this paper, we present a consistent formal semantics
                  (based on our \holocl approach) that includes such a
                  non-strict exception element. We discuss the possible
                  consequences concerning class diagram semantics as well as
                  deduction rules. The benefits of our approach for the
                  specification-pragmatics of design level operation
                  contracts are demonstrated with a small case-study.},
  bibkey = {brucker.ea:ocl-null:2009},
  pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-ocl-null-2009.ps.gz},
  keywords = {\holocl, UML, OCL, null reference, formal semantics},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-ocl-null-2009},
  note = {Best-Paper Award at the OCL 2009 Workshop.}
}
@techreport{wolff:FMWettbebwerb:2009,
  author = {Burkhart Wolff},
  title = {Top-down vs. {B}ottom-up: {F}ormale {M}ethoden im wissenschaftlichen {W}ettbewerb. {E}in essayistischer {S}urvey \"uber den {S}tand der {K}unst.},
  institution = {DFKI Technischer Bericht},
  year = 2009,
  pdf = {http://www.lri.fr/~wolff/papers/other/festschrift.pdf},
  note = {Erschienen in der Festschrift zum 60. Geburtstag von Bernd Krieg-Br\"uckner.},
  abtract = {In diesem Beitrag wird versucht, einen \"Uberblick \"uber
                  den Wettbewerb zweier konkurrierender
                  Forschungsprogramme — genannt Top-down oder
                  Transformationelle Entwicklungsmethodik ver- sus
                  Bottom-up oder post-hoc Programmverifikation — im
                  Bereich “For- maler Methoden” zu geben. Als
                  Einordnungsrahmen benutze ich Laka- tos’s Konzept
                  des “wissenschaftlichen Forschungsprogramms”. Es
                  ergibt sich ein bewusst altmodischer Versuch — im
                  Gegensatz zu modischen bibliometrischen Kriterien
                  (vulgo: Zahlen von Ver\"offentlichungen) —
                  inhaltliche Kriterien f\"ur die Qualit\"at und damit
                  den Fortschritt der wissenschaftlichen Arbeit in
                  unserem Gebiet zu entwickeln.}
}
@inproceedings{SAC,
  author = {F. Za\"idi and A. Cavalli and E. Bayse},
  title = {Network{P}rotocol {I}nteroperability {T}esting based on {C}ontextual},
  booktitle = {24th Annual ACM Symposium on Applied on Applied Computing},
  year = 2009,
  address = {Hawaii, USA},
  month = {March},
  organization = {ACM},
  pages = {2--7}
}
@inproceedings{Haftmann-Wenzel:2009,
  author = {Florian Haftmann and Makarius Wenzel},
  title = {Local theory specifications in {Isabelle/Isar}},
  editor = {Stefano Berardi and Ferruccio Damiani and de Liguoro, Ugo},
  booktitle = {Types for Proofs and Programs, TYPES 2008},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5497},
  year = {2009},
  url = {http://www.lri.fr/~wenzel/papers/local-theory.pdf}
}
@article{oudinet09msr,
  author = {Johan Oudinet},
  title = {Exploration al\'eatoire de mod\`eles},
  journal = {Journal Europ\'een des Syst\`emes Automatis\'es (JESA)},
  year = 2009,
  volume = 43,
  pages = {905--919},
  month = {November},
  note = {Colloque francophone sur la Mod\'elisation des Syst\`emes R\'eactifs},
  annote = {S\'el\'ectionn\'e pour soumission \`a DEDS},
  pdf = {http://www.lri.fr/~oudinet/publis/09/msr09.pdf}
}
@inproceedings{PP_BPZ09,
  author = {L. Bentakouk and P. Poizat and F. Za\"idi},
  title = {A Formal Framework for Service Orchestration Testing based on Symbolic Transition Systems},
  booktitle = {TESTCOM/FATES 2009 - 21th IFIP International Conference on Testing of Communicating Systems},
  pages = {16--32},
  year = 2009,
  volume = 5826,
  series = {Lectures Notes in Computer Science (LNCS)},
  address = {Eindhoven},
  month = {November},
  publisher = {Springer}
}
@inproceedings{LA09,
  author = {Longuet, Delphine and Aiguier, Marc},
  title = {Integration Testing from Structured First-Order Specifications via Deduction Modulo},
  booktitle = {International Conference Theoretical Aspects of Computing (ICTAC 2009)},
  year = {2009},
  pages = {261-276},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {5684},
  abstract = {Testing from first-order specifications has mainly been studied for flat specifications, that are specifications of a single software module. However, the specifications of large software systems are generally built out of small specifications of individual modules, by enriching their union. The aim of integration testing is to test the composition of modules assuming that they have previously been verified, i.e. assuming their correctness. One of the main method for the selection of test cases from first-order specifications, called axiom unfolding, is based on a proof search for the different instances of the property to be tested, thus allowing the coverage of this property. The idea here is to use deduction modulo as a proof system for structured first-order specifications in the context of integration testing, so as to take advantage of the knowledge of the correctness of the individual modules.},
  pdf = {http://www.lri.fr/~longuet/Publications/LA09-ICTAC.pdf}
}
@inproceedings{Wenzel:2009,
  author = {M. Wenzel},
  title = {Parallel Proof Checking in {Isabelle/Isar}},
  booktitle = {ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009)},
  year = 2009,
  editor = {Dos Reis, G. and L. Th\'ery},
  publisher = {ACM Digital Library},
  url = {http://www.lri.fr/~wenzel/papers/parallel-isabelle.pdf}
}
@techreport{approx,
  author = {M.-C. Gaudel and F. Magnez and R. Lassaigne and M. de Rougemont},
  title = {Approximations for Model Checking and Testing (survey, preliminary version)},
  year = {2009},
  month = {May},
  institution = {Universit\'e de Paris-Sud},
  type = {39 pages, under revision},
  x-equipes = {algo fortesse},
  x-type = {article},
  x-support = {rapport},
  pdf = {http://www.lri.fr/~mdr/testing.pdf}
}
@article{daum.ea:fairness:2009,
  author = {Matthias Daum and Jan D\"{o}rrenb\"{a}cher and Burkhart Wolff},
  title = {{P}roving {F}airness and {I}mplementation {C}orrectness of a {M}icrokernel {S}cheduler},
  journal = {Journal of Automated Reasoning (JAR)},
  volume = 42,
  number = {2--4},
  year = 2009,
  pdf = {../papers/journals/pre-fairness.pdf},
  pages = {349--388},
  publisher = {Springer Verlag},
  abstract = {We report on the formal proof of a microkernel's key
                  property, namely the fairness property of its
                  multi-priority process scheduler. The proof
                  architecture links a layer of behavioral reasoning
                  over system-trace sets with a concrete, fairly
                  realistic implementation written in C.  Our
                  microkernel provides an infra-structure for memory
                  virtualization, for communication with hardware
                  devices, for processes (represented as a sequence of
                  assembler instructions, which are executed
                  concurrently over an underlying, formally defined
                  processor), and for inter-process communication
                  (IPC) via synchronous message passing. The kernel
                  establishes process switches according to IPCs and
                  timer-events; however, the scheduling of process
                  switches follows a hierarchy of priorities,
                  favoring, e. g., system processes over application
                  processes over maintenance processes.  Besides the
                  quite substantial models developed in Isabelle/HOL
                  and the formal clarification of their relationship,
                  we provide a detailed analysis what formal
                  requirements a microkernel imposes on the key
                  ingredients (hardware, timers, machine-dependent
                  code) in order to establish the correct operation of
                  the overall system. On the methodological side, we
                  show how early modeling with hindsight to the later
                  verification has substantially helped our project.},
  doi = {10.1007/s10817-009-9119-8},
  note = {G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008).},
  keywords = {Microkernel, Formal verification, Interactive theorem proving, Isabelle/HOL},
  classification = {journal}
}
@inproceedings{Schirmer-Wenzel:2009,
  author = {Norbert Schirmer and Makarius Wenzel},
  title = {State Spaces --- The Locale Way},
  booktitle = {Systems Software Verification (SSV 2009)},
  year = 2009,
  editor = {Ralf Huuck and Gerwin Klein and Bastian Schlich},
  series = {ENTCS},
  publisher = {Elsevier},
  url = {http://www.lri.fr/~wenzel/papers/statespace-locale.pdf}
}
@article{boehme.ea:2009,
  author = {Sascha B\"ohme and Micha{\l} Moskal and Wolfram
                  Schulte and Burkhart Wolff},
  title = {{HOL}-{B}oogie --- {A}n {I}nteractive {P}rover-{B}ackend for the {V}erified {C} {C}ompiler},
  journal = {Journal of Automated Resoning (JAR)},
  year = 2009,
  abstract = {\emph{Boogie} is a verification condition generator for
                  an imperative core language.  It has front-ends for
                  the programming languages C{\#} and C enriched by
                  annotations in first-order logic, ie pre- and
                  postconditions, assertions, and loop invariants.
                  Moreover, concepts like ghost fields, ghost
                  variables, ghost code and speci\-fication functions
                  have been introduced to support a specific modeling
                  methodology.  Boogie's verification conditions ---
                  constructed via a $\mathit{wp}$ calculus from
                  annotated programs --- are usually transferred to
                  automated theorem provers such as \emph{Simplify} or
                  \emph{Z3}. This also comprises the expansion of
                  language-specific modeling constructs in terms of a
                  theory describing memory and elementary operations
                  on it; this theory is called \emph{machine/memory
                  model}.  In this paper, we present a proof
                  environment, HOL-Boogie, that combines Boogie with
                  the interactive theorem prover Isabelle/\HOL, for a
                  specific C front-end and machine/memory model.  In
                  particular, we present specific techniques combining
                  automated and interactive proof methods for code
                  verification. The main goal of our environment is to
                  help program verification engineers in their task to
                  ``debug'' annotations and to find combined proofs
                  where purely automatic proof attempts fail.  },
  doi = {10.1007/s10817-009-9142-9},
  volume = 44,
  number = {1--2},
  pages = {111--144},
  pdf = {../papers/journals/hol-boogie.pdf},
  keywords = {Isabelle/HOL, Theorem proving, Program verification, Memory models, Annotation languages},
  classification = {journal}
}

2008

2008.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2008.bib -c 'year = 2008' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@article{brucker.ea:extensible:2008,
  abstract = {We present an extensible encoding of object-oriented data
		  models into higher-order logic (HOL). Our encoding is
		  supported by a datatype package that leverages the use of
		  the shallow embedding technique to object-oriented
		  specification and programming languages. The package
		  incrementally compiles an object-oriented data model, i.e.,
		  a class model, to a theory containing object-universes,
		  constructors, accessor functions, coercions (casts) between
		  dynamic and static types, characteristic sets, and
		  co-inductive class invariants. The package is conservative,
		  i. e., all properties are derived entirely from constant
		  definitions, including the constraints over object
		  structures. As an application, we use the package for an
		  object-oriented core-language called IMP++, for which we
		  formally prove the correctness of a Hoare logic with
		  respect to a denotational semantics.},
  author = {Achim D. Brucker and Burkhart Wolff},
  journal = {Journal of Automated Reasoning (JAR)},
  classification = {journal},
  language = {USenglish},
  note = {Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds)},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/0_brucker.ea-datatype-2007.pdf},
  title = {{A}n {E}xtensible {E}ncoding of {O}bject-oriented {D}ata {M}odels in {HOL} with an {A}pplication to {IMP++}},
  volume = {Selected Papers of the AVOCS-VERIFY Workshop 2006},
  doi = {10.1007/s10817-008-9108-3},
  pages = {219-249},
  volume = 41,
  number = {3--4},
  year = 2008
}
@incollection{brucker.ea:extensible:2008-b,
  abstract = {We present a datatype package that enables the shallow
		  embedding technique to object-oriented specification and
		  programming languages. This datatype package incrementally
		  compiles an object-oriented data model to a theory
		  containing object-universes, constructors, accessors
		  functions, coercions between dynamic and static types,
		  characteristic sets, their relations reflecting
		  inheritance, and the necessary class invariants. The
		  package is conservative, i.e., all properties are derived
		  entirely from axiomatic definitions. As an application, we
		  use the package for an object-oriented core-language called
		  imp++, for which correctness of a Hoare-Logic with respect
		  to an operational semantics is proven. },
  address = {Paphos, Cyprus},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Proceedings of the European Conference of Object-Oriented
		  Programming (ECOOP 2008)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/978-3-540-70592-5_19},
  editor = {Jan Vitek},
  isbn = {0302-9743},
  language = {USenglish},
  classification = {conference},
  month = {July},
  pages = {438--462},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/brucker.ea-datatype-2008.pdf},
  publisher = {Springer-Verlag},
  series = {LNCS 5142},
  title = {Extensible Universes for Object-Oriented Data Models },
  url = {http://www.springerlink.com/content/416483625116hw37/?p=b2e4cfb4996441a9b171c4594f015499&pi=18},
  year = 2008,
  user = {lukasbru}
}
@inproceedings{brucker.ea:formal:2008,
  title = {{A} {F}ormal {P}roof {E}nvironment for {UML/OCL}},
  abstract = {We present the theorem proving environment HOL-OCL that is
		  integrated in a MDE framework. HOL-OCL allows to reason
		  over UML class models annotated with OCL
		  specifications. Thus, HOL-OCL strengthens a crucial part of
		  the UML to an object-oriented formal method. \holocl
		  provides several derived proof calculi that allow for
		  formal derivations establishing the validity of UML/OCL
		  formulae. These formulae arise naturally when checking the
		  consistency of class models, when formally refining
		  abstract models to more concrete ones or when discharging
		  side-conditions from model-transformations.},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Proceedings of Formal Aspects of Software Engineering
		  (FASE 2008)},
  isbn = {0302-9743},
  language = {USenglish},
  classification = {conference},
  pages = {97--101},
  doi = {10.1007/978-3-540-78743-3_8},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/2008-fase-hol-ocl.pdf},
  publisher = {Springer Berlin / Heidelberg},
  series = {Lecture Notes in Computer Science},
  volume = 4961,
  year = 2008
}
@inproceedings{brucker.ea:verifying:2008,
  abstract = {HOL-TestGen is a specification and test case generation
		  environment extending the interactive theorem prover
		  Isabelle/HOL. The HOL-TestGen method is two-staged: first,
		  the original formula, called test specification, is
		  partitioned into test cases by transformation into a normal
		  form called test theorem. Second, the test cases are
		  analyzed for ground instances (the test data) satisfying
		  the constraints of the test cases. Particular emphasis is
		  put on the control of explicit test hypotheses which can be
		  proven over concrete programs. As such, explicit test
		  hypotheses establish a logical link between validation by
		  test and by proof. Since HOL-TestGen generates explicit
		  test hypotheses and makes them amenable to formal proof,
		  the system is in a unique position to explore the relations
		  between them at an example.},
  address = {Budapest, Hungary },
  author = {Achim D. Brucker and Lukas Br\"ugger and Burkhart Wolff},
  booktitle = {Model-based Testing (MBT) 2008 },
  editor = {Bernd Finkbeiner and Yuri Gurevich and Alexander K.
		  Petrenko},
  language = {USenglish},
  pages = {15-28},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/brucker.ea-testhyps-2008.pdf},
  publisher = {Elsevier Science Publishers },
  series = {Electronic Notes in Theoretical Computer Science},
  title = {Verifying Test-Hypotheses -- An Experiment in Test and
		  Proof},
  year = 2008,
  doi = {10.1016/j.entcs.2008.11.003},
  volume = 202,
  classification = {workshop},
  user = {lukasbru}
}
@incollection{brucker.ea:model-based:2008,
  abstract = {Firewalls are a cornerstone of todays security
		  infrastructure for networks. Their configuration,
		  implementing a firewall policy, is inherently complex, hard
		  to understand, and difficult to validate. We present a
		  substantial case study performed with the model-based
		  testing tool HOL-TestGen. Based on a formal model of
		  firewalls and their policies in HOL, we first present a
		  derived theory for simplifying policies. We discuss
		  different test plans for test specifications. Finally, we
		  show how to integrate these issues to a domain-specific
		  firewall testing tool HOL-TestGen/FW.},
  address = {Tokyo, Japan},
  author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  booktitle = {Testcom/FATES 2008},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/978-3-540-68524-1_9},
  editor = {Kenji Suzuki and Teruo Higashino},
  isbn = {0302-9743 (Print) 1611-3349 (Online)},
  language = {USenglish},
  pages = {103--118},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/2008-testcom-fw-test.pdf},
  publisher = {Springer-Verlag},
  series = {LNCS 5047},
  title = {Model-based Firewall Conformance Testing},
  url = {http://www.springerlink.com/content/5v5167t1216vlw7v/},
  year = 2008,
  classification = {conference},
  user = {lukasbru}
}
@techreport{rasta08cbrTR,
  author = {Alain Denise and Marie-Claude Gaudel and Sandrine-Dominique Gouraud and Richard Lassaigne and Johan Oudinet and Sylvain Peyronnet},
  title = {Coverage-Biased Random Exploration of Large Models and Application to Testing},
  institution = {LRI},
  year = 2008,
  number = 1494,
  address = {Universit\'e Paris-Sud XI},
  month = {June},
  pdf = {http://www.lri.fr/~bibli/Rapports-internes/2008/RR1494.pdf},
  x-equipes = {fortesse bioinfo parall EXT},
  x-type = {article},
  x-support = {rapport}
}
@inproceedings{CG08,
  author = {Ana Cavalcanti and Marie-Claude Gaudel},
  title = {A note on traces refinement and the {\textit{conf}} relation in the
	{U}nifying {T}heories of {P}rogramming},
  booktitle = {Unifying Theories of Programming, Second International Symposium,
	{UTP} 2008, Trinity College, Dublin, {Ireland}, September 8-10, 2008,
	Revised Selected Papers},
  year = {2008},
  editor = {Andrew Butterfield},
  volume = {5713},
  series = {Lecture Notes in Computer Science},
  pages = {42--61},
  publisher = {Springer},
  pdf = {http://www.lri.fr/~mcg/PDF/UTP08.pdf},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {B},
  type_digiteo = {conf_isbn}
}
@inproceedings{PP_CMP08,
  author = {Canal, Carlos and Murillo, {Juan Manuel} and Poizat, Pascal},
  title = {{Practical Approaches for Software Adaptation. Report on the 4th Workshop WCAT at ECOOP 2007}},
  booktitle = {{ECOOP 2007 Workshop Reader}},
  pages = {154--165},
  year = {2008},
  volume = {4906},
  series = {{Lecture Notes in Computer Science}},
  doi = {10.1007/978-3-540-78195-0_15},
  optpdf = {},
  ibiscequipes = {},
  ibisccountry = {},
  ibisckind = {intconf},
  ibisclang = {english},
  ibiscdomain = {}
}
@article{PP_CPS08,
  author = {Canal, Carlos and Poizat, Pascal and Sala{\"u}n, Gwen},
  year = {2008},
  title = {Model-based Adaptation of Behavioural Mismatching Components},
  journal = {IEEE Transactions on Software Engineering},
  pages = {546--563},
  volume = 34,
  number = 4,
  note = {},
  doi = {10.1109/TSE.2008.31},
  optpdf = {},
  ibiscequipes = {},
  ibisckind = {intrevue},
  ibisclang = {english},
  ibiscdomain = {}
}
@inproceedings{PP_CSCPP08,
  author = {Cubo, Javier and Sala{\"u}n, Gwen and Canal, Carlos and Pimentel, Ernesto and Poizat, Pascal},
  year = {2008},
  title = {A Model-Based Approach to the Verification and Adaptation of WF/.NET Components},
  booktitle = {Proceedings of the Workshop on Formal Aspects of Component Software (FACS 07)},
  pages = {39--55},
  volume = {215},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  doi = {doi:10.1016/j.entcs.2008.06.020},
  pdf = {http://www.lri.fr/~poizat/documents/publications/CSCPP08.pdf},
  ibiscequipes = {},
  ibisccountry = {},
  ibisckind = {intconf},
  ibisclang = {english},
  ibiscdomain = {}
}
@inproceedings{FaGaGoMa08,
  author = {J. Fayolle and M.-C. Gaudel and S.-D. Gouraud and B. Marre},
  title = {Statistical Testing of Synchronous Reactive Systems},
  year = {2008},
  booktitle = {ERTS},
  type_digiteo = {conf_autre}
}
@inproceedings{JLdB08,
  author = {Jaghoori, Mohammad Mahdi and Longuet, Delphine and de Boer, Frank S.},
  title = {Schedulability and Compatibility of Real-Time Asynchronous Objects},
  booktitle = {29th IEEE Real-Time Systems Symposium (RTSS 2008)},
  year = {2008},
  pages = {70-79},
  publisher = {{IEEE} Computer Society Press},
  abstract = {We apply automata theory to specifying behavioral interfaces of objects and show how to check schedulability and compatibility of real time asynchronous objects. The behavioral interfaces of real time objects specify (the order and timings of) the messages an object may send and receive. Each object is checked against its behavioral interface; first, to guarantee its correct output behavior, and second to make sure that every message it may receive is processed within the designated deadline (schedulability analysis). Next, we propose a new technique for testing whether every object is used as expected (i.e., according to its behavioral interface) when combined with other objects (compatibility check). Compatibility additionally implies schedulability in the context of the actual system. The analyses are automated using the Uppaal model checker. Our method makes it possible to put a finite bound on the message queue and still obtain schedulability results that are correct for any queue length.},
  pdf = {http://www.lri.fr/~longuet/Publications/JLdB08-RTSS.pdf}
}
@inproceedings{oudinet08movep,
  author = {Johan Oudinet},
  title = {Uniform Random Exploration of Concurrent Systems},
  booktitle = {MOdelling and VErifying parallel Processes (MOVEP)},
  pages = {323--328},
  year = 2008,
  month = {June},
  x-equipes = {fortesse},
  x-type = {article},
  x-support = {actes}
}
@inproceedings{nwesp,
  author = {M. Lallali and F. Zaidi and A. Cavalli},
  title = {Transforming BPEL into Intermediate Format Language For Web Services Composition Testing},
  booktitle = {4th International Conference on Next Generation Web Services Practices},
  year = 2008,
  address = {Seoul},
  month = {October},
  publisher = {IEEE Computer CS},
  note = {191--197},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  pdf = {http://www.lri.fr/~zaidi/pdf_files/nwesp08.pdf},
  x-cle-support = {[B]},
  type_digiteo = {conf_isbn}
}
@inproceedings{ECOWS,
  author = {M. Lallali and F. Zaidi and A. Cavalli and I. Hwang},
  title = {Automatic Timed Test Case Generation for Web Services Composition},
  booktitle = {The 6th IEEE European Conference on Web Services (ECOWS'08)},
  year = 2008,
  editor = {IEEE Computer Society Press},
  address = {Dublin},
  month = {November},
  note = {53--63},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {ECOWS},
  pdf = {http://www.lri.fr/~zaidi/pdf_files/ecows08.pdf},
  type_digiteo = {conf_isbn}
}
@inproceedings{MBT08,
  author = {Marie-Claude Gaudel and Alain Denise and Sandrine-Dominique Gouraud and Richard Lassaigne and Johan Oudinet and Sylvain Peyronnet},
  title = {Coverage-biased random exploration of large models},
  booktitle = {ETAPS Workshop on Model Based Testing},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = 220,
  year = 2008,
  month = {March},
  pages = {3-14},
  note = {invited lecture},
  pdf = {http://www.lri.fr/~mcg/PDF/MBT08.pdf},
  x-equipes = {fortesse bioinfo parall EXT},
  x-type = {invitation},
  x-support = {actes},
  x-cle-support = {B}
}
@incollection{daum.ea:verification:2008,
  abstract = {Though the verification of operating systems is an active
		  research field, a verification method is still missing that
		  provides both, the proximity to practically used
		  programming languages such as C and a realistic model of
		  concurrency, i.e. a model that copes with the granularity
		  of atomic operations actually used in a target machine.Our
		  approach serves as the foundation for the verification of
		  concurrent programs in C0 --- a C fragment enriched by kernel
		  communication primitives --- in a Hoare-Logic. C0 is compiled
		  by a verified compiler into assembly code representing a
		  cooperative concurrent transition system. For the latter,
		  it is shown that it can actually be executed in a true
		  concurrent way reflecting the C0 semantics.},
  author = {Matthias Daum and Jan D\"orrenb\"acher and Mareike Schmidt
		  and Burkhart Wolff},
  booktitle = {Verified Software: Theories, Tools, Experiments},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/978-3-540-87873-5_15},
  language = {USenglish},
  month = {September},
  pages = {161--176},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/1_libvamos.pdf},
  publisher = {Springer Berlin / Heidelberg},
  series = {LNCS 5295},
  title = {A Verification Approach for System-Level Concurrent
		  Programs },
  year = 2008,
  classification = {conference},
  user = {lukasbru}
}
@inproceedings{PP_MPBM08,
  author = {Melliti, Tarek and Poizat, Pascal and {Ben Mokhtar}, Sonia},
  title = {{Distributed Behavioural Adaptation for the Automatic Composition of Semantic Services}},
  booktitle = {{Proceedings of the International Conference on Fundamental Approaches to Software Engineering (FASE 08)}},
  year = {2008},
  pages = {146--162},
  volume = {4961},
  publisher = {Springer},
  series = {{Lecture Notes in Computer Science}},
  doi = {10.1007/978-3-540-78743-3_12},
  pdf = {http://www.lri.fr/~poizat/documents/publications/RR-MPBM07.pdf},
  ibiscequipes = {},
  ibisccountry = {},
  ibisckind = {intconf},
  ibisclang = {english},
  ibiscdomain = {}
}
@inproceedings{PP_MPS08,
  author = {Radu Mateescu and Pascal Poizat and Gwen Sala{\"u}n},
  title = {{Adaptation of Service Protocols using Process Algebra and On-the-Fly Reduction Techniques}},
  booktitle = {Proceedings of the International Conference on Service Oriented Computing (ICSOC 08)},
  pages = {84--99},
  year = 2008,
  publisher = {Springer},
  volume = {5364},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-540-89652-4_10},
  optpdf = {},
  ibiscequipes = {},
  ibisccountry = {},
  ibisckind = {intconf},
  ibisclang = {english},
  ibiscdomain = {}
}
@inproceedings{PP_BP08,
  author = {Sandrine Beauche and Pascal Poizat},
  title = {{Automated Service Composition with Adaptive Planning}},
  booktitle = {Proceedings of the International Conference on Service Oriented Computing (ICSOC 08)},
  pages = {530--537},
  year = 2008,
  publisher = {Springer},
  volume = {5364},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/978-3-540-89652-4_42},
  pdf = {http://www.lri.fr/~poizat/documents/publications/RR-BP08.pdf},
  ibiscequipes = {},
  ibisccountry = {},
  ibisckind = {intconf},
  ibisclang = {english},
  ibiscdomain = {}
}
@incollection{bohme.ea:hol-boogie:2008,
  abstract = {Boogie is a program verification condition generator for
		  animperative core language. It has front-ends for the
		  programming languagesC# and C enriched by annotations in
		  first-order logic.Its verification conditions --- constructed
		  via a wp calculus from these annotations --- are usually
		  transferred to automated theorem proverssuch as Simplify or
		  Z3. In this paper, however, we present a
		  proof-environment,HOL-Boogie, that combines Boogie with the
		  interactivetheorem prover Isabelle/HOL. In particular, we
		  present specific techniquescombining automated and
		  interactive proof methods for code-verification.We will
		  exploit our proof-environment in two ways: First, we
		  present scenariosto \"debug\" annotations (in particular:
		  invariants) by interactiveproofs. Second, we use our
		  environment also to verify \"background theories\",i.e.
		  theories for data-types used in annotations as well as
		  memoryand machine models underlying the verification method
		  for C.},
  address = {Montreal, Canada},
  author = {Sascha B\"ohme and Rustan Leino and Burkhart Wolff},
  booktitle = {21th International Conference on Theorem proving in
		  Higher-Order Logics (TPHOLs 2008)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/978-3-540-71067-7_15},
  editor = {Sofiene Tahar and Otmane Ait Mohamed and C{\'e}sar
		  Mu{\~n}oz},
  language = {USenglish},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/boehme_tphols_2008.pdf},
  publisher = {Springer-Verlag},
  series = {LNCS 5170},
  title = {{HOL-Boogie} --- {A}n {I}nteractive {P}rover for the {B}oogie {P}rogram {V}erifier},
  year = 2008,
  user = {lukasbru}
}

2007

2007.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2007.bib -c 'year = 2007' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{ICFEM07,
  author = {A. Cavalcanti and M.-C. Gaudel},
  title = {Testing for Refinement in {CSP}},
  booktitle = {Formal Methods and Software Engineering, ICFEM 2007},
  publisher = {Springer Verlag},
  volume = 4789,
  series = {Lecture Notes in Computer Science},
  year = {2007},
  pages = {151-170},
  pdf = {http://www.lri.fr/~mcg/PDF/GaudelCSPreport.pdf}
}
@incollection{brucker.ea:test-sequence:2007,
  abstract = {HOL-TestGen is a specification and test-case generation
		  environment extending the interactive theorem prover
		  Isabelle/HOL. Its method is two-staged: first, the original
		  formula is partitioned into test cases by transformation
		  into a normal form. Second, the test cases are analyzed for
		  ground instances (the test data) satisfying the constraints
		  of the test cases. Particular emphasis is put on the
		  control of explicit test hypotheses which can be proven
		  over concrete programs.
		  
		  Although originally designed for black-box unit-tests,
		  HOL-TestGen's underlying logic and deduction engine is
		  powerful enough to be used in test-sequence generation, too.
		  
		  We develop the theory for test-sequence generation with
		  HOL-TestGen and describe its use in a substantial
		  case-study in the field of computer security, namely the
		  black-box test of configured firewalls. },
  keywords = {security, model-based testing, specification-based
		  testing, firewall testing},
  paddress = {Heidelberg},
  address = {Zurich},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {{TAP} 2007: Tests And Proofs},
  copyright = {\copyright Springer-Verlag},
  copyrighturl = {http://link.springer-ny.com/link/service/series/0558/},
  language = {USenglish},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 4454,
  editor = {Bertrand Meyer and Yuri Gurevich},
  project = {CSFMDOS},
  title = {Test-Sequence Generation with HOL-TestGen -- With an
		  Application to Firewall Testing },
  categories = {holtestgen},
  classification = {conference},
  year = 2007,
  doi = {10.1007/978-3-540-73770-4_9},
  pages = {149--168},
  isbn = {978-3-540-73769-8},
  classification = {conference},
  pdf = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.ps.gz},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007}
}
@article{brucker.ea:mda:2007,
  abstract = {We present a model-driven architecture (MDA) framework
		  that integrates formal analysis techniques into an
		  industrial software development process model. This
		  comprises modeling using UML/OCL, processing models by
		  model transformations, code generation (including
		  runtime-test environments) and formal analysis using the
		  theorem proving environment HOL-OCL. Moreover, our
		  frameworks supports the verification of proof obligations
		  that are generated during model transformations.We show the
		  extensibility of our approach by providing a SecureUML
		  extension of the framework, which allows for an integrated
		  specification of security properties, their analysis and
		  their conversion to code.},
  author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  journal = {Electronic Communications of the EASST},
  language = {USenglish},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2007/easst-framework.pdf},
  title = {An {MDA} Framework Supporting {OCL}},
  url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/12},
  volume = 5,
  year = 2007,
  classification = {workshop},
  user = {doserj}
}
@article{brucker.ea:semantic:2007,
  abstract = {We report on the results of a long-term project to
		  formalize the semantics of OCL 2.0 in Higher-order Logic
		  (HOL). The ultimate goal of the project is to provide a
		  formalized, machine-checked semantic basis for a theorem
		  proving environment for OCL (as an example for an
		  object-oriented specification formalism) which is as
		  faithful as possible to the original informal semantics. We
		  report on various (minor) inconsistencies of the OCL
		  semantics, discuss the more recent attempt to align the OCL
		  semantics with UML 2.0 and suggest several extensions which
		  make, in our view, OCL semantics more fit for future
		  extensions towards program verifications and specification
		  refinement.},
  author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  journal = {Electronic Communications of the EASST},
  language = {USenglish},
  url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/12},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2007/easst-glitches.pdf},
  title = {Semantic Issues of {OCL}: Past, Present, and Future},
  volume = 5,
  year = 2007,
  classification = {ejournal},
  user = {doserj}
}
@inproceedings{AALGL07,
  author = {Aiguier, Marc and Arnould, Agn{\`e}s and Le Gall, Pascale and Longuet, Delphine},
  title = {Test Selection Criteria for Quantifier-Free First-Order Specifications},
  booktitle = {International Symposium on Fundamentals of Software Engineering (FSEN 2007)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4767},
  year = {2007},
  pages = {144-159},
  ee = {http://dx.doi.org/10.1007/978-3-540-75698-9_10},
  abstract = {This paper deals with test case selection from axiomatic
specifications whose axioms are quantifier-free first-order formulae. Test
cases are modeled as ground formulae and any specification has an exhaustive
test data set whose successful submission means correctness,
provided that the software under verification can be modeled as a firstorder
structure over the same signature. As it has already been done for
positive conditional equational specifications, we derive test cases from
selection criteria based on axiom coverage. Our selection criteria allows
us to select test cases by iteratively unfolding an initial target test purpose,
given as a formula. The initial reference test set is iteratively split
into successive subsets. Each subset of test cases is defined by constraints
which are increasingly introduced by the unfolding procedure to ensure
an appropriate matching between the current test purpose under unfolding
and specification axioms. Our unfolding procedure is sound (no test
is added) and complete (no test is lost) with respect to the starting test
purpose. It is exemplified on a simple example.},
  pdf = {http://www.lri.fr/~longuet/Publications/AALL07-FSEN.pdf}
}
@inproceedings{AL07,
  author = {Aiguier, Marc and Longuet, Delphine},
  title = {Test Selection Criteria for Modal Specifications of Reactive Systems},
  booktitle = {First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007)},
  year = {2007},
  pages = {159-170},
  ee = {http://doi.ieeecomputersociety.org/10.1109/TASE.2007.52},
  abstract = {In the framework of functional testing from algebraic specifications, the strategy of test selection which has been widely and efficiently applied is based on axiom unfolding. In this paper, we propose to extend this selection strategy to a modal formalism used to specify dynamic and reactive systems. Such a work is then a first step to tackle testing of such systems more abstractly than most of the works dealing with what is called conformance testing. We get a higher level of abstraction since our specifications account for what is usually called underspecification, i.e. they do not denote a unique model but a class of models. Hence, the testing process can be applied at every design level.},
  pdf = {http://www.lri.fr/~longuet/Publications/AL07-TASE.pdf}
}
@article{PP_APS07,
  author = {Attiogb{\'e}, Christian and Poizat, Pascal and Sala{\"u}n, Gwen},
  ibiscequipes = {},
  year = {2007},
  title = {A Formal and Tool-Equipped Approach for the Integration of State Diagrams and Formal Datatypes},
  ibisckind = {intrevue},
  ibisclang = {english},
  journal = {IEEE Transactions on Software Engineering},
  ibiscdomain = {},
  pages = {157--170},
  volume = {33},
  number = {3},
  doi = {10.1109/TSE.2007.21},
  optpdf = {}
}
@inproceedings{BCDMPT07a,
  author = {Becker, Steffen and Canal, Carlos and Diakov, Nikolay and Murillo, Juan Manuel and Poizat, Pascal and Tivoli, Massimo},
  ibiscequipes = {},
  year = {2007},
  ibisccountry = {},
  title = {Coordination and Adaptation Techniques: Bridging the Gap Between Design and Implementation},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {ECOOP 2006 Workshop Reader},
  ibiscdomain = {},
  pages = {72--86},
  volume = {4379},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  doi = {10.1007/978-3-540-71774-4_9},
  optpdf = {}
}
@inproceedings{PP_CSCPP07,
  author = {Cubo, Javier and Sala{\"u}n, Gwen and Canal, Carlos and Pimentel, Ernesto and Poizat, Pascal},
  ibiscequipes = {},
  year = {2007},
  ibisccountry = {},
  title = {Relating Model-Based Adaptation and Implementation Platforms: A Case Study with WF/.NET 3.0},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the 12th International Workshop on Component-Oriented Programming (WCOP 07)},
  ibiscdomain = {},
  pages = {9--13},
  pdf = {http://www.lri.fr/~poizat/documents/publications/CSCPP07.pdf},
  pages = {155--170},
  volume = {182},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier}
}
@article{basin.ea:verifying:2007,
  abstract = {We report on a case study in applying different formal
		  methods to model and verify an architecture for
		  administrating digital signatures. The architecture
		  comprises several concurrently executing systems that
		  authenticate users and generate and store digital
		  signatures by passing security relevant data through a
		  tightly controlled interface. The architecture is
		  interesting from a formal-methods perspective as it
		  involves complex operations on data as well as process
		  coordination and hence is a candidate for both
		  data-oriented and process-oriented formal methods.We have
		  built and verified two models of the signature architecture
		  using two representative formal methods. In the first, we
		  specify a data model of the architecture in Z that we
		  extend to a trace model and interactively verify by theorem
		  proving. In the second, we model the architecture as a
		  system of communicating processes that we verify by
		  finite-state model checking. We provide a detailed
		  comparison of these two different approaches to
		  formalization (infinite state with rich data types versus
		  finite state) and verification (theorem proving versus
		  model checking). Contrary to common belief, our case study
		  suggests that Z is well suited for temporal reasoning about
		  process models with complex operations on data. Moreover,
		  our comparison highlights the advantages of proving
		  theorems about such models and provides evidence that, in
		  the hands of an experienced user, theorem proving may be
		  neither substantially more time-consuming nor more complex
		  than model checking.},
  author = {David Basin and Hironobu Kuruma and Kunihiko Miyazaki and
		  Kazuo Takaragi and Burkhart Wolff},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/s00165-006-0012-5},
  journal = {Formal Aspects of Computing},
  language = {USenglish},
  month = {March},
  note = {http://www.springerlink.com/content/u368650p18557674/?p=8851693f5ba14a3fb9d493dae37783b8&pi=0},
  number = 1,
  pages = {63--91},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2007/fac.submit.pdf},
  title = {Verifying a signature architecture: a comparative case
		  study},
  volume = 19,
  year = 2007,
  user = {lukasbru}
}
@article{basin.ea:z:2007,
  abstract = {Z is a standardized and well-established formal
		  specification language originally developed in the 80ies by
		  researchers at oxford University. Although the original
		  emphasis of Z is on specification, the semantics for Z can
		  be expressed within higher-order logic (HOL). On this
		  basis, a theorem-proving environment such as Isabelle/HOL-Z
		  can be built. In this paper, we show how properties over
		  specifications can be formally proven in HOL-Z. Particular
		  emphasis is put on proving relationships between
		  specification such as refinement.},
  author = {David Basin and Hironobu Kuruma and Shin Nakajima and
		  Burkhart Wolff},
  url = {http://www.jstage.jst.go.jp/browse/jssst/24/2/_contents},
  journal = {Computer Software --- Journal of the Japanese Society for
		  Software Science and Technology},
  language = {USenglish},
  month = {April},
  note = {In Japanese. },
  number = 2,
  pages = {21--26},
  title = {{T}he {Z} {S}pecification {L}anguage and the {P}roof {E}nvironment {Isabelle/HOL-Z}},
  volume = 24,
  year = 2007,
  user = {wolff}
}
@techreport{rapport-lri,
  author = {F. Zaidi and Mounir Lallali},
  title = {Use of Verification Techniques for Components Testing},
  institution = {LRI, http://www.lri.fr/Rapports-internes},
  year = 2007,
  number = 1465,
  address = {Universit{\'e} Paris-Sud XI},
  month = {January},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {rapport}
}
@inproceedings{PP_HP07,
  author = {Haddad, Serge and Poizat, Pascal},
  ibiscequipes = {},
  year = {2007},
  ibisccountry = {},
  title = {Transactional Reduction of Component Compositions},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the IFIP International Conference on Formal Methods for Networked and Distributed Systems (FORTE 07)},
  ibiscdomain = {},
  pages = {341--357},
  volume = {4574},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  doi = {10.1007/978-3-540-73196-2_22},
  pdf = {http://www.lri.fr/~poizat/documents/publications/HP07.pdf}
}
@mastersthesis{oudinet07mthesis,
  author = {Johan Oudinet},
  title = {Uniform random walks in concurrent models},
  school = {Universit{\'e} Paris-Sud 11, LRI},
  year = 2007,
  month = {September},
  pdf = {http://www.lri.fr/~oudinet/publis/07/mthesis.pdf}
}
@mastersthesis{oudinet07mthesis-fr,
  author = {Johan Oudinet},
  title = {Tirages al{\'e}atoires uniformes dans des syst{\`e}mes concurrents},
  school = {Universit{\'e} Paris-Sud 11, LRI},
  year = 2007,
  month = {September},
  pdf = {http://www.lri.fr/~oudinet/publis/07/mthesis-fr.pdf},
  slides = {http://www.lri.fr/~oudinet/publis/07/mthesis-fr-slides.pdf},
  abstract = {Ce rapport pr{\'e}sente les premiers r{\'e}sultats
                  exp{\'e}rimentaux sur la g{\'e}n{\'e}ration
                  al{\'e}atoire uniforme de chemins dans de tr{\`e}s
                  grands graphes qui mod{\'e}lisent des syst{\`e}mes
                  concurrents, comme elle a {\'e}t{\'e}
                  pr{\'e}sent{\'e}e dans [5]. L'approche se base sur
                  des techniques de comptage et de tirage
                  al{\'e}atoire uniforme dans des structures
                  combinatoires et sur le fait que dans des
                  syst{\`e}mes construits {\`a} partir de composants
                  concurrents, il est possible de combiner
                  astucieusement des tirages uniformes dans les
                  composants pour approcher, avec une tr{\`e}s bonne
                  approximation, un tirage uniforme dans le
                  syst{\`e}me global. Ce rapport d{\'e}crit les
                  impl{\'e}mentations des m{\'e}thodes propos{\'e}es
                  dans [5], analyse les r{\'e}sultats d'une suite de
                  tests de performance, et g{\'e}n{\'e}ralise le cas
                  o{\`u} les composants concurrents se synchronisent
                  {\`a} plusieurs symboles et plusieurs occurrences de
                  synchronisations.}
}
@inproceedings{oudinet07rt,
  author = {Johan Oudinet},
  title = {Uniform Random Walks in Very Large Models},
  booktitle = {RT '07: Proceedings of the 2nd international workshop on Random testing},
  year = 2007,
  month = {November},
  address = {Atlanta, GA, USA},
  publisher = {ACM Press},
  pages = {26--29},
  pdf = {http://www.lri.fr/~oudinet/publis/07/rt07-oudinet.pdf},
  slides = {http://www.lri.fr/~oudinet/publis/07/rt07-slides.pdf},
  x-equipes = {fortesse},
  x-type = {articlecourt},
  x-support = {actes},
  x-cle-support = {B},
  abstract = { This paper presents first experimental results on
                  uniform random generation of paths in very large
                  graphs that model concurrent systems, as it was
                  presented in [3].  The approach is based on
                  techniques and tools for counting and drawing
                  uniformly at random in combinatorial structures.  It
                  exploits the fact that in a system made of several
                  concurrent components, local uniform drawings of
                  component paths can be combined into a very good
                  approximation of uniform drawing of paths in the
                  global system, without constructing the global
                  model.  The paper describes some implementation of
                  the methods presented in [3], reports results on a
                  first suite of benchmarks, exploring the limits and
                  the possibility of this new approach to uniform
                  random walks.  }
}
@phdthesis{Longuet07,
  author = {Longuet, Delphine},
  title = {Test \`a partir de sp\'ecifications axiomatiques},
  school = {Laboratoire IBISC, Universit\'e d'\'Evry-Val d'Essonne},
  year = {2007},
  abstract = {My work is dedicated to the definition of a formal framework for testing dynamic systems from logical specifications. In the framework of algebraic specifications, one of the methods that has extensively been studied, called axiom unfolding, consists in deriving test cases from the specification axioms. The thesis has then been aimed at generalising and adapting this selection method to specifications expressed in more general logics than equational logic: first-order logic and first-order modal logic. Thanks to this last extension, we propose a new approach for testing dynamic systems, the usual approach, called conformance testing, using an automata-based description of the system under test.},
  pdf = {http://www.lri.fr/~longuet/Publications/TheseLonguet.pdf}
}
@inproceedings{LA07,
  author = {Longuet, Delphine and Aiguier, Marc},
  title = {Specification-Based Testing for {C}o{C}asl's Modal Specifications},
  booktitle = {Second International Conference on Algebra and Coalgebra in Computer Science (CALCO 2007)},
  publisher = {Springer},
  series = {Lecture Notes in Computer Science},
  volume = {4624},
  year = {2007},
  pages = {356-371},
  ee = {http://dx.doi.org/10.1007/978-3-540-73859-6_24},
  abstract = {Specification-based testing is a particular case of black-box
testing, which consists in deriving test cases from an analysis of a formal
specification. We present in this paper an extension of the most
popular and most efficient selection method widely used in the algebraic
framework, called axiom unfolding, to coalgebraic specifications, using
the modal logic provided by the CoCasl specification language.},
  pdf = {http://www.lri.fr/~longuet/Publications/LA07-CALCO.pdf}
}
@inproceedings{mounir,
  author = {M. Lallali and F. Zaidi and A. Cavalli},
  title = {Timed Modeling of Web Services Composition for Automatic Testing},
  booktitle = {SITIS IEEE/ACM 2007},
  type_digiteo = {conf_isbn},
  pages = {417--427},
  year = 2007,
  address = {Shanghai},
  month = {December},
  publisher = {IEEE Computer Society},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  pdf = {http://www.lri.fr/~zaidi/pdf_files/SITIS07.pdf},
  x-cle-support = {SITIS}
}
@techreport{rapport-mounir,
  author = {M. Lallali and F. Zaidi and A. Cavalli},
  title = {Timed Modeling of Web Services Composition for Automatic Testing},
  institution = {GET/INT},
  year = 2007,
  number = {07008-LOR},
  address = {Evry},
  month = {September},
  note = {Long version},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {rapport}
}
@incollection{survey,
  author = {M.-C. Gaudel and P. Le Gall},
  booktitle = {Formal Methods and Testing, R. Hierons, J. Bowen, and M. Harman,eds},
  title = {Testing Data Types Implementations from Algebraic Specifications},
  publisher = {Springer-Verlag},
  volume = 4949,
  series = {Lecture Notes in Computer Science},
  year = 2007,
  note = {209-239},
  pdf = {http://www.lri.fr/~mcg/PDF/surveyTestTAA.pdf}
}
@incollection{wenzel.ea:building:2007,
  abstract = {We present the generic system framework of
		  Isabelle/Isarunderlying recent versions of Isabelle. Among
		  other things, Isar provides an infrastructure for Isabelle
		  plug-ins, comprising extensible state components and
		  extensible syntax that can be bound to tactical ML
		  programs. Thus the Isabelle/Isar architecture may be
		  understood as an extension and refinement of the
		  traditional "LCF approach", with explicit infrastructure
		  for building derivative systems. To demonstrate the
		  technical potential of the framework, we apply it to a
		  concrete formalmethods tool: the HOL-Z 3.0 environment,
		  which is geared towards the analysis of Z specifications
		  and formal proof of forward-refinements.},
  author = {Makarius Wenzel and Burkhart Wolff},
  booktitle = {TPHOLs 2007},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/978-3-540-74591-4_26},
  editor = {Klaus Schneider and Jens Brandt},
  language = {USenglish},
  pages = {351--366},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2007/tphols07.submission.pdf},
  publisher = {Springer-Verlag},
  series = {LNCS 4732},
  title = {Building Formal Method Tools in the Isabelle/Isar
		  Framework},
  year = 2007,
  classification = {conference},
  user = {wolff}
}
@inproceedings{PP_MPS07,
  author = {Mateescu, Radu and Poizat, Pascal and Sala{\"u}n, Gwen},
  ibiscequipes = {},
  year = {2007},
  ibisccountry = {},
  title = {Behavioral Adaptation of Component Compositions based on Process Algebra Encodings},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE 07)},
  ibiscdomain = {},
  pages = {385--388},
  organization = {ACM,IEEE},
  doi = {10.1145/1321631.1321690},
  pdf = {http://www.lri.fr/~poizat/documents/publications/RR-MPS07.pdf}
}
@inproceedings{IJCAI07,
  author = {Nicolas Baskiotis and
               Mich{\`e}le Sebag and
               Marie-Claude Gaudel and
               Sandrine-Dominique Gouraud},
  title = {A Machine Learning Approach for Statistical Software Testing},
  booktitle = {IJCAI, Proceedings of the 20th International Joint
               Conference on Artificial Intelligence},
  year = {2007},
  pages = {2274-2279},
  pdf = {http://www.ijcai.org/papers07/Papers/IJCAI07-366.pdf}
}
@inproceedings{PP_PS07,
  author = {Poizat, Pascal and Sala{\"u}n, Gwen},
  ibiscequipes = {},
  year = {2007},
  ibisccountry = {},
  title = {Adaptation of Open Component-based Systems},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS 07)},
  ibiscdomain = {},
  pages = {141--156},
  volume = {4468},
  series = {Lecture Notes in Computer Science},
  publisher = {Springer},
  doi = {10.1007/978-3-540-72952-5_9},
  pdf = {http://www.lri.fr/~poizat/documents/publications/PS07.pdf}
}
@inproceedings{PP_PST07,
  author = {Poizat, Pascal and Sala{\"u}n, Gwen and Massimo Tivoli},
  ibiscequipes = {},
  year = {2007},
  ibisccountry = {},
  title = {An Adaptation-based Approach to Incrementally Build Component Systems},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the International Workshop on Formal Aspects of Component Software (FACS 06)},
  ibiscdomain = {},
  pages = {155--170},
  volume = {182},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2006.09.037},
  pdf = {http://www.lri.fr/~poizat/documents/publications/PST07.pdf}
}

2006

2006.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2006.bib -c 'year = 2006' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@proceedings{garca.ea:proceedings:2006,
  abstract = {This book constitutes the refereed proceedings of the
		  International Workshop on Formal Aspects of Testing and
		  Runtime Verification, FATES/RV 2006, held in Seattle, USA
		  in August 2006 in conjuction with FLoC.The 14 revised full
		  papers presented together with twoinvited papers were
		  carefully reviewed and selected from 34 submissions. },
  address = {Seattle, USA},
  copyright = {\ Springer-Verlag},
  editor = {Manuel N{\'u}{\~n}ez Garc{\'\i}a and Klaus Havelund and
		   Grigore Rosu and Burkhart Wolff},
  copyrighturl = {http://dx.doi.org/10.1007/11940197},
  doi = {10.1007/11940197},
  language = {USenglish},
  note = {LNCS 4262.},
  publisher = {Springer Verlag},
  title = {Proceedings of the International Workshop on Formal
		  Aspects of Testing and Runtime Verification (FATES/RV)},
  year = 2006,
  classification = {workshop},
  user = {wolff}
}
@inproceedings{DeGaGoLaPe06,
  author = {A. Denise and  M.-C. Gaudel and S.-D. Gouraud and R. Lassaigne and S. Peyronnet},
  title = {Uniform Random Sampling of Traces in Very Large Models},
  booktitle = {1st ACM International Workshop on Random Testing (RT)},
  year = {2006},
  pages = {10-19},
  type_digiteo = {conf_isbn}
}
@techreport{DeGaGoLaPe1445,
  author = {A. Denise and  M.-C. Gaudel and S.-D. Gouraud and R. Lassaigne and S. Peyronnet},
  title = {Uniform Random Sampling of Traces in Very Large Models},
  year = {2006},
  number = {1445},
  address = {Universit\'e Paris-Sud 11},
  pdf = {http://www.lri.fr/~gouraud/papers/RR1445.pdf}
}
@inproceedings{lassos,
  author = {A. Denise and M.-C. Gaudel and S.-D. Gouraud and R. Lasseigne and S. Peyronnet },
  title = {Uniform Random Sampling of Traces in very Large Models},
  booktitle = {1st International ACM Workshop on Random Testing},
  year = 2006,
  month = {July},
  pages = {10 -19},
  pdf = {http://www.lri.fr/~mcg/PDF/108.pdf}
}
@techreport{brucker.ea:hol-ocl-book:2006,
  author = {Achim D. Brucker and Burkhart Wolff},
  institution = {ETH Z{\"u}rich},
  language = {USenglish},
  title = {The {HOL-OCL} {B}ook},
  classification = {unrefereed},
  categories = {holocl},
  year = 2006,
  number = 525,
  pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf},
  abstract = {HOL-OCL is an interactive proof environment for the Object
		  Constraint Language (OCL). It is implemented as a shallow
		  embedding of OCL into the Higher-order Logic (HOL) instance
		  of the interactive theorem prover Isabelle. HOL-OCL defines
		  a machine-checked formalization of the semantics as
		  described in the standard for OCL 2.0. This conservative,
		  shallow embedding of UML/OCL into Isabelle/HOL includes
		  support for typed, extensible UML data models supporting
		  inheritance and subtyping inside the typed lambda-calculus
		  with parametric polymorphism. As a consequence of
		  conservativity with respect to higher-order logic (HOL), we
		  can guarantee the consistency of the semantic model.
		  Moreover, HOL-OCL provides several derived calculi for
		  UML/OCL that allow for formal derivations establishing the
		  validity of UML/OCL formulae. Elementary automated support
		  for such proofs is also provided top },
  bibkey = {brucker.ea:hol-ocl-book:2006},
  keywords = {security, SecureUML, UML, OCL, HOL-OCL,
		  model-transformation}
}
@incollection{brucker.ea:package:2006,
  author = {Achim D. Brucker and Burkhart Wolff},
  title = {A Package for Extensible Object-Oriented Data Models with
		  an Application to IMP++},
  editor = {Abhik Roychoudhury and Zijiang Yang},
  booktitle = {International Workshop on Software Verification and
		  Validation (SVV 2006)},
  year = 2006,
  series = {Computing Research Repository (CoRR)},
  month = aug,
  address = {Seattle, USA},
  language = {USenglish},
  abstract = {We present a datatype package that enables the use of
		  shallow embedding technique to object-oriented
		  specification and programming languages. The package
		  incrementally compiles an object-oriented data model to a
		  theory containing object-universes, constructors, and
		  accessor functions, coercions between dynamic and static
		  types, characteristic sets, their relations reflecting
		  inheritance, and the necessary class invariants. The
		  package is conservative, i.e., all properties are derived
		  entirely from axiomatic definitions. As an application, we
		  use the package for an object-oriented core-language called
		  \IMPOO, for which correctness of a Hoare logic with respect
		  to an operational semantics is proven.},
  categories = {holocl},
  ps = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.ps.gz},
  pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf},
  classification = {workshop},
  keywords = {datatype package, extensible object-oriented data model,
		  object-oriented specification,shallow embedding}
}
@inproceedings{brucker.ea:mda:2006,
  abstract = {We present an MDA framework, developed in the functional
		  programming language SML, that tries to bridge the gap
		  between formal software development and the needs of
		  industrial software development, e.g., code generation.
		  Overall, our tool-chain provides support for software
		  modeling using UML/OCL and guides the user from
		  type-checking and model transformations to code generation
		  and formal analysis of the UML/OCL model. We conclude with
		  a report on our experiences in using a functional language
		  for implementing MDA tools. },
  author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  booktitle = {6th OCL Workshop at the UML/MoDELS Conference},
  language = {USenglish},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2006/OclApps-framework.pdf},
  title = {An {MDA} Framework Supporting{ OCL}},
  classification = {workshop},
  year = 2006,
  user = {wolff}
}
@inproceedings{brucker.ea:semantic:2006,
  abstract = {We report on the results of a long-term project to
		  formalize the semantics of OCL 2.0 in Higher-order Logic
		  (HOL). The ultimate goal of the project is to provide a
		  formalized, machine-checked semantic basis for a theorem
		  proving environment for OCL (as an example for an
		  object-oriented specification formalism) which is as
		  faithful as possible to the original informal semantics. We
		  report on various (minor) inconsistencies of the OCL
		  semantics, discuss the more recent attempt to align the OCL
		  semantics with UML 2.0 and suggest several extensions which
		  make, in our view, OCL semantics more fit for future
		  extensions towards programming-like verifications and
		  specification refinement, which are, in our view, necessary
		  to make OCL more fit for future extensions. },
  author = {Achim D. Brucker and J\"urgen Doser and Burkhart Wolff},
  booktitle = {6th OCL Workshop at the UML/MoDELS Conference},
  language = {USenglish},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2006/OclApps-glitches.pdf},
  title = {Semantic Issues of {OCL}: Past, Present, and Future},
  year = 2006,
  url = {http://eceasst.cs.tu-berlin.de/index.php/eceasst/issue/view/12},
  classification = {conference},
  user = {wolff}
}
@incollection{brucker.ea:model:2006,
  abstract = { SecureUML is a security modeling language for formalizing
		  access control requirements in a declarative way. It is
		  equipped with a \UML notation in terms of a \UML profile,
		  and can be combined with arbitrary design modeling
		  languages. We present a semantics for SecureUML in terms of
		  a model transformation to standard \acs{uml}/\acs{ocl}. The
		  transformation scheme is used as part of an implementation
		  of a tool chain ranging from front-end visual modeling
		  tools over code-generators to the interactive theorem
		  proving environment \holocl. The methodological
		  consequences for an analysis of the generated \OCL formulae
		  are discussed.},
  address = {Genova},
  author = {Achim D. Brucker and J{\"u}rgen Doser and Burkhart Wolff},
  booktitle = {{MoDELS} 2006: Model Driven Engineering Languages and
		  Systems},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/11880240_22},
  editor = {Oscar Nierstrasz and Jon Whittle and David Harel and
		  Gianna Reggio},
  filelabel = {Extended Version},
  language = {USenglish},
  note = {An extended version of this paper is available as ETH
		  Technical Report, no. 524.},
  pages = {306--320},
  publisher = {Springer-Verlag},
  series = {LNCS 4199},
  title = {A Model Transformation Semantics and Analysis Methodology
		  for {SecureUML}},
  year = 2006,
  pdf = {http://www.lri.fr/~wolff/papers/conf/brucker-2.ea-transformation-2006.pdf},
  user = {wolff},
  classification = {conference}
}
@inproceedings{ABL06,
  author = {Aiguier, Marc and Bahrami, Diane and Longuet, Delphine},
  title = {An Abstract Way to Define Rewriting Logic},
  booktitle = {IPM International Workshop on Foundations of Software Engineering (FSEN 2005)},
  series = {Electronic Notes in Theoretical Computer Science},
  volume = {159},
  year = {2006},
  pages = {205-226},
  ee = {http://dx.doi.org/10.1016/j.entcs.2005.09.033},
  abstract = {Since rewriting logic has been introduced, it has shown its adequateness both as a semantic and a logical framework. But the numerous applications of the rewriting logic in the above two areas has shown the importance of increasing its expressive power. Therefore, in order to facilitate this work, we will study in this paper how to generalize the transformation that from equational logic has resulted in the rewriting logic. To achieve this purpose, we will show that there exists a valid and useful notion of rewriting logic associated to any rewriting theory fitting an abstract framework developed by two of the authors in previous papers.},
  pdf = {http://www.lri.fr/~longuet/Publications/ABL05-FSEN.pdf}
}
@article{IBISC:PP_CMP06b,
  author = {Canal, Carlos and Murillo, Juan Manuel and Poizat, Pascal},
  ibiscequipes = {},
  year = {2006},
  title = {Software Adaptation},
  ibisckind = {natrevue},
  ibisclang = {english},
  journal = {L'Objet},
  ibiscdomain = {},
  pages = {9--31},
  volume = {12},
  number = {1},
  pdf = {http://www.lri.fr/~poizat/documents/publications/CMP06b.pdf}
}
@inproceedings{PP_CPS06b,
  author = {Canal, Carlos and Poizat, Pascal and Sala\"un, Gwen},
  ibiscequipes = {},
  year = {2006},
  ibisccountry = {Italy},
  title = {Synchronizing Behavioural Mismatch in Software Composition},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the 8th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)},
  ibiscdomain = {},
  pages = {63--77},
  volume = {4037},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/11768869_7},
  pdf = {http://www.lri.fr/~poizat/documents/publications/CPS06b.pdf}
}
@inproceedings{PP_CPS06a,
  author = {Canal, Carlos and Poizat, Pascal and Sala\"un, Gwen},
  ibiscequipes = {},
  year = {2006},
  ibisccountry = {France},
  title = {Adaptation de composants logiciels. Une approche automatis\'{e}e bas\'{e}e sur des expressions r\'{e}guli\`{e}res de vecteurs de synchronisation},
  ibisckind = {natconf},
  ibisclang = {francais},
  booktitle = {Actes de la Premi\`{e}re Conf\'{e}rence Francophone sur les Architectures Logicielles (CAL)},
  ibiscdomain = {},
  pages = {}
}
@inbook{PP_FHP06,
  author = {Frappier, Marc and Habrias, Henri and Poizat, Pascal},
  ibiscequipes = {},
  year = {2006},
  title = {Software Specification Methods: an Overview Using a Case Study},
  chapter = {19 - A Comparison of the Specification Methods},
  ibisckind = {chapitre},
  ibisclang = {english},
  ibiscdomain = {},
  pages = {},
  publisher = {ISTE, Hermes Science Publishing}
}
@techreport{priorites,
  author = {G. Lestiennes and M.-C. Gaudel },
  title = {Mod\'elisation et Test de Syst\`emes comportant des actions prioritaires},
  institution = {Universit\'e de Paris-Sud},
  year = 2006,
  month = {march},
  type = {Rapport {LRI}},
  number = 1434,
  pdf = {http://www.lri.fr/~mcg/PDF/RapportEntreesPrioritaires.pdf}
}
@incollection{encyclo,
  author = {Gaudel, M.-C.},
  booktitle = {Encyclop\'edie de l{'}informatique et des syst\`emes d{'}information},
  title = {Validation et V\'erification},
  publisher = {Vuibert},
  year = 2006,
  pages = {1136-1150},
  comment = {VetV080705ter.doc}
}
@incollection{ICC,
  author = {Gaudel, M.-C.},
  booktitle = {Communication, Connaissance : supports et m\'ediations \`a l{'}\^age de l{'}information, J.-G. Ganascia, ed.},
  title = {Les objets \`a l{'}\'epreuve des faits},
  publisher = {CNRS \'Editions},
  year = 2006,
  note = {4 pages},
  comment = {http://www.lri.fr/~mcg/PDF/ObjetsICC1205.pdf}
}
@inbook{PP_HPF06,
  author = {Habrias, Henri and Poizat, Pascal and Frappier, Marc},
  ibiscequipes = {},
  year = {2006},
  title = {Software Specification Methods: an Overview Using a Case Study},
  chapter = {20 - Glossary},
  ibisckind = {chapitre},
  ibisclang = {english},
  ibiscdomain = {},
  pages = {},
  publisher = {ISTE, Hermes Science Publishing}
}
@inbook{IBISC:PP_Poi06,
  author = {Poizat, Pascal},
  ibiscequipes = {},
  year = {2006},
  title = {Software Specification Methods: an Overview Using a Case Study},
  chapter = {12 - SDL},
  ibisckind = {chapitre},
  ibisclang = {english},
  ibiscdomain = {},
  pages = {},
  publisher = {ISTE, Hermes Science Publishing}
}
@article{PP_PR06,
  author = {Poizat, Pascal and Royer, Jean-Claude},
  ibiscequipes = {},
  year = {2006},
  title = {A Formal Architectural Description Language based on Symbolic Transition Systems and Modal Logic},
  ibisckind = {intrevue},
  ibisclang = {english},
  journal = {Journal of Universal Computer Science (J.UCS)},
  ibiscdomain = {},
  pages = {1741--1782},
  volume = {12},
  number = {12},
  pdf = {http://www.jucs.org/jucs_12_12/a_formal_architectural_description}
}
@inproceedings{PP_PRS06,
  author = {Poizat, Pascal and Royer, Jean-Claude and Sala\"un, Gwen},
  ibiscequipes = {},
  year = {2006},
  ibisccountry = {Italy},
  title = {Bounded Analysis and Decomposition for Behavioural Descriptions of Components},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the 8th International Conference on Formal Methods for Open Object-Based Distributed Systems (FMOODS)},
  ibiscdomain = {},
  pages = {33--47},
  volume = {4037},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/11768869_5},
  pdf = {http://www.lri.fr/~poizat/documents/publications/PRS06.pdf}
}
@inproceedings{PP_PST06,
  author = {Poizat, Pascal and Sala\"un, Gwen and Tivoli, Massimo},
  ibiscequipes = {},
  year = {2006},
  ibisccountry = {France},
  title = {On Dynamic Reconfiguration of Behavioural Adaptation},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the third International Workshop on Coordination and Adaptation Techniques for Software Entities (WCAT 06)},
  ibiscdomain = {},
  pages = {61--69},
  pdf = {http://www.lri.fr/~poizat/documents/publications/PST06.pdf}
}
@inbook{PP_PV06,
  author = {Poizat, Pascal and Vergnaud, Thomas},
  ibiscequipes = {},
  year = {2006},
  title = {M\'ethodes formelles pour les syst\`emes r\'epartis et coop\'eratifs},
  chapter = {5 - Langages de description d'architecture},
  ibisckind = {chapitre},
  ibisclang = {francais},
  ibiscdomain = {},
  pages = {},
  publisher = {Hermes, Lavoisier}
}
@inproceedings{hut,
  author = {S. Maag and F. Zaidi},
  title = {A Step-Wise Validation Approach for a Wireless Routing Protocol},
  booktitle = {IEEE International Conference on Communications and Electronics (ICCE'06)},
  year = {2006},
  address = {Hanoi, Vietnam},
  month = {October},
  publisher = {IEEE},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  x-cle-support = {HUT/ICCE}
}
@inproceedings{mswim06,
  author = {S. Maag and F. Zaidi},
  title = {Testing methodology for an ad hoc routing protocol},
  key = {isbn:1-59593-502-9},
  booktitle = {PM2HW2N '06: Proceedings of the ACM international workshop on Performance monitoring, measurement, and evaluation of heterogeneous wireless and wired networks},
  pages = {48--55},
  year = 2006,
  address = {Terromolinos, Spain},
  publisher = {ACM},
  note = {http://doi.acm.org/10.1145/1163653.1163663},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  pdf = {http://www.lri.fr/~zaidi/pdf_files/mswim06.pdf},
  x-cle-support = {PM2HW2N}
}
@techreport{olsr,
  author = {S. Maag and F. Zaidi},
  title = { Sp{\'e}cification Formelle pour le Test d'un Protocole de Routage ad hoc},
  institution = {GET/INT},
  year = 2006,
  number = {06009-LOR},
  address = {France},
  month = {October},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {rapport}
}
@inproceedings{GoGo06,
  author = {S.-D. Gouraud and A. Gotlieb},
  title = {Using CHRs to generate functional test cases for the Java Card
Virtual Machine},
  booktitle = {8th International Symposium on Practical Aspects of Declarative
Languages (PADL)},
  series = {LNCS 3819},
  year = {2006},
  pages = {1-15},
  pdf = {http://www.lri.fr/~gouraud/papers/GoGo06.pdf},
  type_digiteo = {conf_isbn}
}

2005

2005.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2005.bib -c 'year = 2005' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@article{CMZal,
  author = {A. Cavalli and A. Mederreg and F. Zaidi and P. Combes and W. Monin and R. Castanet and M. MacKaya and P. Laurencot},
  title = {Une {P}late-forme de {V}alidation {M}ulti-{S}ervices et {M}ulti-{P}rotocoles  - {R}{\'e}sultats d'{E}xp{\'e}rimentations},
  journal = {Annales des T{\'e}l{\'e}communications},
  year = 2005,
  volume = 60,
  number = {5-6},
  pages = {588--609},
  month = {June},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {revue},
  x-cle-support = {JSAT}
}
@inproceedings{notere,
  author = {A. Cavalli and S. Maag and F. Zaidi},
  title = {Une approche UML pour la validation des services web},
  booktitle = {5{\`e}me Colloque international sur les NOuvelles TEchnologies de la REpartition (NOTERE)},
  year = 2005,
  month = {September},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {actes},
  pdf = {http://www.lri.fr/~zaidi/pdf_files/notere05.pdf},
  x-cle-support = {NOTERE}
}
@techreport{brucker.ea:hol-testgen:2005,
  author = {Achim D. Brucker and Burkhart Wolff},
  institution = {Computer Security Group, ETH Z\"urich},
  language = {USenglish},
  month = {apr},
  number = 482,
  title = {{HOL-TestGen} 1.0.0 User Guide},
  classification = {unrefereed},
  year = 2005,
  user = {wolff}
}
@incollection{brucker.ea:interactive:2005,
  abstract = {HOL-TestGen is a test environment for specification-based
		  unit testing build upon the proof assistant Isabelle/HOL\@.
		  While there is considerable skepticism with regard to
		  interactive theorem provers in testing communities, we
		  argue that they are a natural choice for (automated)
		  symbolic computations underlying systematic tests. This
		  holds in particular for the development on non-trivial
		  formal test plans of complex software, where some parts of
		  the overall activity require inherently guidance by a test
		  engineer. In this paper, we present the underlying methods
		  for both black box and white box testing in interactive
		  unit test scenarios. HOL-TestGen can also be understood as
		  a unifying technical and conceptual framework for
		  presenting and investigating the variety of unit test
		  techniques in a logically consistent way. },
  address = {Edinburgh},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Formal Approaches to Testing of Software (FATES 05)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/11759744_7},
  editor = {Wolfgang Grieskamp and Carsten Weise},
  isbn = {3-540-25109-X},
  language = {USenglish},
  pages = {87--102},
  publisher = {Springer-Verlag},
  series = {LNCS 3997},
  title = {{I}nteractive {T}esting using {HOL-TestGen}},
  year = 2005,
  classification = {workshop},
  user = {wolff}
}
@incollection{brucker.ea:symbolic:2005,
  abstract = {We present a method for the automatic generation of test
		  cases for HOL formulae containing primitive recursive
		  predicates. These test cases can be used for the animation
		  of specifications as well as for black-box testing of
		  external programs. Our method is two-staged: first, the
		  original formula is partitioned into test cases by
		  transformation into a Horn-clause normal form (HCNF).
		  Second, the test cases are analyzed for instances with
		  constant terms satisfying the premises of the clauses.
		  Particular emphasis is put on the control of test
		  hypotheses and test hierarchies to avoid intractability. We
		  applied our method to several examples, including AVL-trees
		  and the red-black tree implementation in the standard
		  library from SML/NJ. },
  address = {Linz 04},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Formal Approaches to Testing of Software (FATES 04)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/b106767},
  editor = {Jens Grabowski and Brian Nielsen},
  isbn = {3-540-25109-X},
  language = {USenglish},
  pages = {16--32},
  publisher = {Springer-Verlag},
  series = {LNCS 3395},
  title = {Symbolic Test Case Generation for Primitive Recursive
		  Functions},
  url = {http://springerlink.metapress.com/content/yqv0ajk1wb0ctllt/?p=4f2d15532c2c45e6a0673b2465e27f5e&pi=1},
  year = 2005,
  classification = {workshop},
  user = {wolff}
}
@article{brucker.ea:verification:2005,
  abstract = {We present a method for the security analysis of realistic
		  models over off-the-shelf systems and their configuration
		  by formal, machine-checked proofs. The presentation follows
		  a large case study based on a formal security analysis of a
		  CVS-Server architecture.\\\\The analysis is based on an
		  abstract architecture (enforcing a role-based access
		  control), which is refined to an implementation
		  architecture (based on the usual discretionary access
		  control provided by the \posix{} environment). Both
		  architectures serve as a skeleton to formulate access
		  control and confidentiality properties.\\\\Both the
		  abstract and the implementation architecture are specified
		  in the language Z. Based on a logical embedding of Z into
		  Isabelle/HOL, we provide formal, machine-checked proofs for
		  consistency properties of the specification, for the
		  correctness of the refinement, and for security properties.},
  author = {Achim D. Brucker and Burkhart Wolff},
  copyright = {\copyright Springer-Verlag},
  issn = {1433-2779},
  journal = {International Journal on Software Tools for Technology
		  Transfer (STTT)},
  language = {USenglish},
  number = 3,
  doi = {10.1007/s10009-004-0176-3},
  pages = {233--247},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2005/sttt_03.pdf},
  title = {A Verification Approach for Applied System Security},
  volume = 7,
  year = 2005,
  classification = {journal},
  user = {wolff}
}
@inproceedings{ALGLT05,
  author = {Aiguier, Marc and Le Gall, Pascale and Longuet, Delphine and Touil, Assia},
  title = {A Temporal Logic for Input Output Symbolic Transition Systems},
  booktitle = {12th Asia-Pacific Software Engineering Conference (APSEC 2005)},
  year = {2005},
  pages = {43-50},
  ee = {http://doi.ieeecomputersociety.org/10.1109/APSEC.2005.19},
  abstract = {In this paper, we present a temporal logic called
F whose interpretation is over Input Output Symbolic Transition
Systems (IOSTS). IOSTS extend transition systems to
communications and data in order to tackle communications
with system environment. F is then defined as an extension of
temporal logic CTL* (a temporal logic which mixes together
the features of Linear Temporal Logic (LTL) and Computational
Temporal Logic (CTL)). Three basic properties are established on
F: adequacy and preservation of properties along synchronized
product and IOSTS refinement.},
  pdf = {http://www.lri.fr/~longuet/Publications/AGLLT05-APSEC.pdf}
}
@thesis{wolff05,
  author = {Burkhart Wolff},
  title = {Correct Tools for Formal Methods in Software Engineering},
  publisher = {Universit{\"a}t Freiburg},
  year = 2005,
  language = {USEnglish},
  abstract = {The development of \emph{tools} for program analysis,
		  verification and refinement is a prerequisite for the
		  proliferation of formal methods in industry and research.
		  While most tools were directly implemented in a programming
		  language, the ultimate goal of this work is to represent
		  widely known formal methods in a so-called \emph{logical
		  framework} \textbf{by their semantics} using a particular
		  representation technique --- called \emph{shallow
		  embedding} --- motivated by more efficient deduction. Based
		  on this representation, symbolic computations in tool
		  implementations can be based on formally proven correct
		  \emph{derived rules}. As such, this correctness-oriented
		  approach has been known for a while and has been criticized
		  for a number of shortcomings: \begin{enumerate} \item the
		  application range of embeddings in logical frameworks is
		  limited to very small and artificially designed languages,
		  \item their application is impossible when the formal
		  specification method is still under development, \item
		  embedding the semantics conservatively and deriving some
		  rules on this basis does not imply that there is a
		  comprehensive support of a method that is technically
		  powerful enough for applications, \item the integration in
		  a more global software engineering process and its
		  pragmatics is too difficult, and \item the usability of
		  embeddings is doubtful even if one is targeting at the
		  (fairly small market of) proof environments.
		  \end{enumerate} In contrast to this criticism, we claim
		  that our approach is feasible. We substantiate this by
		  developing: \begin{enumerate} \item suitable embeddings for
		  widely used formal methods, including process-oriented,
		  data-oriented and object-oriented specification methods
		  (CSP, Z, UML/OCL), \item abstractions and aspect-oriented
		  structuring techniques allowing for the quick development
		  of semantic variants enabling the study consequences of
		  changes in formal methods under development (like UML/OCL),
		  \item particular techniques for generating library
		  theories, for supporting particular deduction styles in
		  proofs, for specialized deduction support for concrete
		  development methodologies, \item different scenarios of the
		  integration of the developed tools in conventional tool
		  chains in software engineering, and \item front-ends for
		  light-weight integration into tool chains (like HOL-Z 2.0)
		  or prototypic encapsulation of logical embeddings into
		  generic graphical user-interfaces for a more comprehensive
		  encapsulation. \end{enumerate} Finally, we validate one of
		  these tool chains (HOL-Z 2.0) by a substantial case-study
		  in the field of computer security. },
  note = {Habilitationsschrift},
  classification = {book},
  url = {http://www.inf.ethz.ch/~bwolff/habil/schrift.pdf}
}
@article{atomic,
  author = {C. Jones and D. Lomet and A. Romanovsky and G. Weikum and A. Fekete and M.-C. Gaudel and H. F. Korth and R. de Lemos and E. Moss and R. Rajwar and K. Ramamritham and B. Randell and L. Rodrigues},
  title = {The Atomic Manifesto: a Story in Four Quarks},
  journal = {Journal of Universal Computer Science},
  year = {2005},
  volume = {11},
  number = {5},
  pages = {636-650},
  pdf = {http://www.lri.fr/~mcg/PDF/AtomicManifesto.pdf}
}
@inproceedings{PP_CMP05,
  author = {Canal, Carlos and Murillo, Juan Manuel and Poizat, Pascal},
  ibiscequipes = {},
  year = {2005},
  ibisccountry = {Norway},
  title = {Coordination and Adaptation Techniques for Software Entities},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {European Conference on Object-Oriented Programming (ECOOP) 2004 Workshop Reader},
  ibiscdomain = {},
  pages = {133--147},
  volume = {3344},
  series = {Lecture Notes in Computer Science},
  doi = {10.1007/b104146},
  pdf = {http://www.lri.fr/~poizat/documents/publications/CMP05.pdf}
}
@incollection{aspinall.ea:assisted:2005,
  title = {{A}ssisted {P}roof {D}ocument {A}uthoring},
  abstract = {Significant advances have been made in formalised
		  mathematical texts for large, demanding proofs. But
		  although such large developments are possible, they still
		  take an inordinate amount of effort and there is a
		  significant gap between the resulting formalised
		  machinecheckable proof scripts and the corresponding
		  human-readable mathematical texts. We present an authoring
		  system for formal proof which addresses these concerns. It
		  is based on a central document format which, in the
		  tradition of literate programming, allows one to extract
		  either a formal proof script or a human-readable document;
		  the two may have differing structure and detail levels, but
		  are developed together in a synchronised way. Additionally,
		  we introduce ways to assist production of the central
		  document, by allowing tools to contribute backflow to
		  update and extend it. Our authoring system builds on the
		  new PG Kit architecture for Proof General, bringing the
		  extra advantage that it works in a uniform interface,
		  generically across various interactive theorem provers.},
  author = {David Aspinall and Christoph L\"uth and Burkhart Wolff},
  booktitle = {Fourth International Conference on Mathematical Knowledge
		  Management (MKM 05)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/11618027_5},
  language = {USenglish},
  publisher = {Springer Verlag},
  pdf = {http://www.lri.fr/~wolff/papers/conf/aspinall-authoring-mkm-06.pdf},
  series = {LNCS 3863.},
  year = 2005,
  classification = {conference}
}
@techreport{basin.ea:specifying:2005,
  abstract = {We report on a case-study in using the data-oriented
		  modeling language Z to formalize a security architecture
		  for administering digital signatures and its architectural
		  security requirements. Within an embedding of Z in the
		  higher-order logic Isabelle/HOL, we provide formal
		  machine-checked proofs of the correctness of the
		  architecture with respect to its requirements. A
		  formalization and verification of the same architecture has
		  been previously carried out using the process-oriented
		  modeling language PROMELA and the SPIN model checker. We
		  use this as a basis for comparing these two different
		  approaches to formalization (infinite state with rich data
		  types versus finite state) and verification (theorem
		  proving versus model checking).},
  author = {David Basin and Hironobu Kuruma and Kazuo Takaragi and
		  Burkhart Wolff},
  institution = {Computer Security Group, ETH Z\"urich},
  language = {USenglish},
  month = 1,
  number = 471,
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2005/HSD.pdf},
  title = {{S}pecifying and {V}erifying {H}ysteresis {S}ignature {S}ystem with {HOL-Z}},
  year = 2005,
  user = {wolff}
}
@incollection{basin.ea:verification:2005,
  abstract = {We report on a case study in using HOL-Z, an embedding of
		  Z in higher-order logic, to specify and verify a security
		  architecture for administering digital signatures. We have
		  used HOL-Z to formalize and combine both data-oriented and
		  process-oriented architectural views. Afterwards, we
		  formalized temporal requirements in Z and carried out
		  verification in higher-order logic. The same architecture
		  has been previously verified using the SPIN model checker.
		  Based on this, we provide a detailed comparison of these
		  two di erent approaches to formalization (infinite state
		  with rich data types versus finite state) and verification
		  (theorem proving versus model checking). Contrary to common
		  belief, our case study suggests that Z is well suited for
		  temporal reasoning about process models with rich data.
		  Moreover, our comparison highlights the advantages of this
		  approach and provides evidence that, in the hands of
		  experienced users, theorem proving is neither substantially
		  more time-consuming nor more complex than model checking.},
  author = {David Basin and Hironobu Kuruma and Kazuo Takaragi and
		  Burkhart Wolff },
  booktitle = {Formal Methods 2005},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/11526841_19},
  language = {USenglish},
  pages = {269--285},
  publisher = {Springer Verlag},
  series = {LNCS 3582},
  title = {{V}erification of a {S}ignature {A}rchitecture with {HOL-Z}},
  pdf = {http://www.lri.fr/~wolff/papers/conf/Basin-Verification-FM05.pdf},
  year = 2005,
  user = {wolff}
}
@incollection{bayse,
  author = {E. Bayse and A. Cavalli and M. Nunez and F. Zaidi},
  title = {A Passive Testing Approach based on Invariants: application to the WAP},
  booktitle = {Computer Networks},
  publisher = {Elsevier Science},
  year = {2005},
  volume = {48},
  pages = {247-266},
  x-equipes = {fortesse EXT},
  x-type = {article},
  x-support = {revue},
  pdf = {http://www.lri.fr/~zaidi/pdf_files/CN05.pdf},
  x-cle-support = {TN}
}
@article{MSR,
  author = {G. Lestiennes and M.-C. Gaudel },
  title = {Test de syst\`emes r\'eactifs non r\'eceptifs},
  journal = {Journal Europ\'en des Syst\`emes automatis\'es},
  year = {2005},
  volume = {36},
  number = {1-2-3},
  pages = {255-270},
  note = {proceedings of MSR'05},
  pdf = {http://www.lri.fr/~mcg/PDF/MSR2005.pdf}
}
@inproceedings{FME05,
  author = {Gaudel, M.-C.},
  title = {Formal Methods and Testing: Hypotheses, and Correctness Approximations},
  booktitle = {FM 2005: Formal Methods: International Symposium of Formal Methods},
  publisher = {Springer Verlag},
  volume = 3582,
  series = {Lecture Notes in Computer Science},
  year = {2005},
  pages = {2-8},
  note = {keynote talk},
  pdf = {http://www.lri.fr/~mcg/PDF/gaudelFME05.pdf}
}
@inproceedings{undo,
  author = {Gaudel, M.-C.},
  title = {Toward Undoing in Composite Web Services},
  booktitle = {Architecting Dependable Systems III},
  publisher = {Springer Verlag},
  volume = 3549,
  series = {Lecture Notes in Computer Science},
  year = 2005,
  pages = {59-68},
  pdf = {http://www.lri.fr/~mcg/PDF/UndoLast.pdf}
}
@mastersthesis{Longuet05,
  author = {Longuet, Delphine},
  title = {Une th\'eorie du raffinement orient\'ee propri\'et\'es pour les automates communicants},
  school = {Laboratoire de M\'ethodes Informatiques (LaMI), Universit\'e d'\'Evry-Val d'Essonne},
  year = {2005},
  abstract = {The aim of this thesis was, on the one hand, to define a refinement theory in the frame of the formalism of communicating automata extended to data (EIOLTS) and on the other hand, to define an axiomatic formalism dedicated to the specification of reactive systems, whose semantics is based on these communicating automata.},
  pdf = {http://www.lri.fr/~longuet/Publications/DEALonguet.pdf}
}
@inproceedings{PP_PNPR05,
  author = {Pavel, Sebastian and Noy\'{e}, Jacques and Poizat, Pascal and Royer, Jean-Claude},
  ibiscequipes = {},
  year = {2005},
  ibisccountry = {},
  title = {Java Implementation of a Component Model with Explicit Symbolic Protocols},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Software Composition (SC)},
  ibiscdomain = {},
  pages = {115--124},
  volume = {3628},
  series = {Lecture Notes in Computer Science},
  pdf = {http://www.lri.fr/~poizat/documents/publications/PNPR05.pdf},
  doi = {10.1007/11550679_9}
}
@techreport{Go1400,
  author = {S.-D. Gouraud},
  title = {AuGuSTe: a Tool for Statistical Testing (Experimental results)},
  year = {2005},
  number = {1400},
  address = {Universit\'e Paris-Sud 11},
  pdf = {http://www.lri.fr/~gouraud/papers/gouraud_RR1400.pdf}
}
@inproceedings{GoGo05,
  author = {S.-D. Gouraud and A. Gotlieb},
  title = {Utilisation des CHRs pour g\'en\'erer des cas de test
pour la Machine Virtuelle Java Card},
  booktitle = {Journ\'ees Francophones de Programmation par Contraintes
(JFPC)},
  year = {2005},
  pages = {383-392},
  pdf = {http://www.lri.fr/~gouraud/papers/GoGo05.pdf},
  type_digiteo = {conf_autre}
}
@techreport{GoGo1725,
  author = {S.-D. Gouraud and A. Gotlieb},
  title = {Using CHRs to Generate Functional Test Cases for the Java Card Virtual
Machine},
  year = {2005},
  number = {1725},
  pdf = {http://www.lri.fr/~gouraud/papers/GoGo_PI1725.pdf}
}
@inproceedings{PP_SP05,
  author = {Sala{\"u}n, Gwen and Poizat, Pascal},
  ibiscequipes = {},
  year = {2005},
  ibisccountry = {},
  title = {Interacting Extended State Diagrams},
  ibisckind = {intconf},
  ibisclang = {english},
  booktitle = {Proceedings of the International Workshop on Semantic Foundations of Engineering Design Languages (SFEDL 04)},
  ibiscdomain = {},
  pages = {49--57},
  volume = {115},
  series = {Electronic Notes in Theoretical Computer Science},
  publisher = {Elsevier},
  doi = {10.1016/j.entcs.2004.09.028},
  pdf = {http://www.lri.fr/~poizat/documents/publications/SP05.pdf}
}
@incollection{meyer.ea:tactic-based:2005,
  abstract = {Within a framework of correct code-generation from
		  HOLspecifications, we present a particular instance
		  concerned with the optimized compilation of a lazy language
		  (called MiniHaskell) to a strict language (called MiniML).
		  Both languages are defined as shallow embeddings into
		  denotational semantics based on Scott s cpo s, leading to a
		  derivation of the corresponding operational semantics in
		  order to cross-check the basic definitions. On this basis,
		  translation rules from one language to the other were
		  formally derived in Isabelle/HOL. Particular emphasis is
		  put on the optimized compilation of function applications
		  leading to the side-calculi inferring e.g. strictness of
		  functions. The derived rules were grouped and set-up as an
		  instance of our generic, tactic-based translator for
		  specifications to code.},
  author = {Thomas Meyer and Burkhart Wolff},
  booktitle = {Types for Proofs and Programs (TYPES 2004)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/11617990_13},
  editor = {Jean-Christophe Filliatre and Christine Paulin and
		  Benjamin Werner},
  language = {USenglish},
  month = 8,
  pages = {202--215},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2005/2_optcom.pdf},
  publisher = {Springer Verlag},
  series = {LNCS 3839},
  title = {Tactic-based Optimized Compilation of Functional
		  Programs},
  year = 2005,
  classification = {workshop},
  user = {wolff}
}

2004

2004.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2004.bib -c 'year = 2004' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{platonis,
  author = {A. Cavalli and A. Mederreg and F. Zaidi and P. Combes and W. Monin and R. Castanet and M. Mackaya and P. Laurencot},
  title = {A Multi-Service and Multi-Protocol Validation Platform Experimentation Results},
  booktitle = {Testing of Communicating Systems (Testcom'04) },
  year = {2004},
  editor = {R. Hierons and R. Groz},
  series = {LNCS 2978},
  month = {March},
  pages = {17--19},
  organization = {The 16th IFIP International Conference, TestCom},
  publisher = {Springer}
}
@article{brasil,
  author = {A. Cavalli and A. Mederreg and F. Za{\"i}di},
  title = {Application of a formal testing methodology to wireless telephony networks},
  journal = {International Journal of the Brazilian Computer Society (JCBS)},
  year = 2004,
  volume = 10,
  number = 2,
  pages = {56-68},
  month = {November},
  note = {ISSN 0104-6500}
}
@inproceedings{CMPVZ-edutech04,
  author = {A. Cavalli and S. Maag and S. Papagiannaki and G. Vergiakis and F. Za{\"i}di},
  title = {A {T}esting {M}ethodology for an {O}pen {S}oftware {E}-{L}earning {P}latform},
  booktitle = {18th IFIP World Computer congress-TC10/WG10.5 Workshop Edutech},
  pages = {165-174},
  year = 2004,
  address = {Toulouse, France},
  month = {August}
}
@inproceedings{DeGaGo04,
  author = {A. Denise and M.-C. Gaudel and S.-D. Gouraud},
  title = {A generic method for statistical testing},
  booktitle = {15th. IEEE International Symposium on Software Reliability Engineering (ISSRE)},
  year = {2004},
  pages = {25-34},
  pdf = {http://www.lri.fr/~gouraud/papers/DeGaGo04.pdf},
  type_digiteo = {conf_isbn}
}
@techreport{DeGaGo1386,
  author = {A. Denise and M.-C. Gaudel and S.-D. Gouraud},
  title = {A Generic Method For Statistical Testing},
  year = {2004},
  number = {1386}
}
@inproceedings{DeniseGG04,
  author = {A. Denise and M.-C. Gaudel and S.-D. Gouraud},
  title = {A Generic Method for Statistical Testing},
  booktitle = {IEEE Int. Symp. on Software Reliability Engineering (ISSRE)},
  year = {2004},
  pages = {25-34},
  pdf = {http://www.lri.fr/~mcg/PDF/articleISSRE04.pdf}
}
@techreport{brucker.ea:symbolic:2004,
  abstract = {We present a method for the automatic generation of test
		  cases for HOL formulae containing primitive recursive
		  predicates. These test cases may be used for the animation
		  of specifications as well as for black-box-testing of
		  external programs.\\\\Our method is two-staged: first, the
		  original formula is partitioned into test cases by
		  transformation into a Horn-clause normal form (CNF).
		  Second, the test cases are analyzed for ground instances
		  satisfying the premises of the clauses. Particular emphasis
		  is put on the control of test hypothesis' and test
		  hierarchies to avoid intractability.\\\\We applied our
		  method to several examples, including AVL-trees and the
		  red-black implementation in the standard library from SML/NJ.},
  author = {Achim D. Brucker and Burkhart Wolff},
  institution = {Computer Security Group, ETH Z\"urich},
  language = {USenglish},
  month = {jun},
  number = 449,
  title = {Symbolic Test Case Generation for Primitive Recursive
		  Functions},
  year = 2004,
  classification = {unrefereed},
  user = {wolff}
}
@techreport{rauch.ea:formalizing:2004,
  abstract = {We present a formal model of Java two’s-complement
		  integral arithmetics. The model directly formalizes the
		  artihmetic operations as given in the Java Language
		  Specification (JLS). The algebraic properties of these
		  definitions are derived. Underspecifications and
		  ambiguities in the JLS are pointed out and clarified. The
		  theory is formally analyzed in Isabelle/HOL that is,
		  machine-checked proofs for the ring properties and
		  divisor/remainder theorems etc. are provided. This work is
		  suited to build the framework for machine-supported
		  reasoning over arithmetic formulae in the context of Java
		  source-code verification. },
  author = {Nicole Rauch and Burkhart Wolff},
  institution = {ETH Z\"urich},
  language = {USenglish},
  month = 11,
  number = 458,
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2004/root.pdf},
  title = {Formalizing Java's Two's-Complement Integral Type in
		  Isabelle/HOL},
  year = 2004,
  classification = {unrefereed},
  user = {wolff}
}
@inproceedings{Go04,
  author = {S.-D. Gouraud},
  title = {AuGuSTe: un outil pour le Test Statistique},
  booktitle = {Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels (AFADL)},
  year = {2004},
  pages = {337-340},
  type_digiteo = {conf_autre}
}
@phdthesis{Gouraud04,
  author = {S.-D. Gouraud},
  title = {Utilisation des Structures Combinatoires pour le Test Statistique},
  school = {Universit\'e Paris-Sud 11, LRI},
  year = {2004},
  pdf = {http://www.lri.fr/~gouraud/papers/these_gouraud.pdf}
}

2003

2003.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2003.bib -c 'year = 2003' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@proceedings{basin.ea:theorem:2003,
  abstract = {This book constitutes the refereed proceedings of the 16th
		  International Conference on Theorem Proving in Higher Order
		  Logics, TPHOLs 2003, held in Rome, Italy in September 2003.
		  The 24 revised full papers presented together with an
		  invited paper were carefully reviewed and selected from 50
		  submissions. The papers are organized in topical sections
		  on hardware and Assembler languages, proof automation, fool
		  combination, logic extensions, theorem prover technology,
		  mathematical theories, and security. Among the theorem
		  proving systems discussed are HOL, Coq, MetaPRL, and
		  Isabelle/Isar.Geschrieben f\"ur:Researchers and
		  professionalsSchlagworte: automated deduction formal
		  methods formal verification hardware verification
		  higher-order logic logic design mathematical logic model
		  checking program verification proof theory theorem provers
		  theorem proving unification},
  address = {Rome, Italy},
  copyright = {\ Springer-Verlag},
  doi = {10.1007/b11935},
  editor = {David Basin and Burkhart Wolff},
  language = {USenglish},
  month = {Sep},
  note = {LNCS 2758.},
  publisher = {Springer-Verlag},
  title = {{T}heorem {P}roving in {H}igher {O}rder {L}ogics, 16th {I}nternational {C}onference ({TPHOL}s 2003)},
  year = 2003,
  user = {wolff}
}
@techreport{platonis02v2,
  author = { Fatiha Za{\"i}di},
  title = {Platonis - rapport final},
  year = 2003,
  type = {Delivrable},
  institution = {Institut National des T{\'e}l{\'e}communications, France}
}
@inproceedings{CMZ-I2TS03,
  author = {A. Cavalli and A. Mederreg and F. Za{\"i}di},
  title = {Application of Formal Testing Methodology to Wireless Telephony Networks},
  booktitle = {2nd International Information and Telecommunications TEchnologies Symposium, I2TS'2003},
  year = 2003,
  address = {Florianopolis, Brazil},
  month = {October}
}
@inproceedings{CMZal-cfip03,
  author = {A. Mederreg and F. Za{\"i}di and P. Combes and W. Monin and R. Castanet and M. MacKaya and P. Lauren{\~c}ot},
  title = {Une {P}late-forme de {V}alidation {M}ulti-{S}ervices et {M}ulti-{P}rotocoles  - {R}{\'e}sultats d'{E}xp{\'e}rimentations},
  booktitle = {CFIP'2003 Ing{\'e}nierie des Protocoles},
  pages = {135--151},
  year = 2003,
  editor = {A. Cavalli, M. Riguidel et A. Serhouchni},
  address = {Paris},
  month = {October},
  publisher = {Herm{\`e}s}
}
@incollection{brucker.ea:using:2003,
  abstract = { Tools for a specification language can be implemented
		  \emph{directly} (by building a special purpose theorem
		  prover) or \emph{by a conservative embedding} into a typed
		  meta-logic, which allows their safe and logically
		  consistent implementation and the reuse of existing theorem
		  prover engines. For being useful, the conservative
		  extension approach must provide derivations for several
		  thousand ``folklore'' theorems.\\\\In this paper, we
		  present an approach for deriving the mass of these theorems
		  mechanically from an existing library of the meta-logic.
		  The approach presupposes a structured \emph{theory
		  morphism} mapping library datatypes and library functions
		  to new functions of the specification language while
		  uniformly modifying some semantic properties; for example,
		  new functions may have a different treatment of
		  undefinedness compared to old ones.},
  address = {Nijmegen},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Types 2002, Proceedings of the workshop Types for Proof
		  and Programs},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/3-540-45685-6_8},
  editor = {Herman Geuvers and Freek Wiedijk},
  isbn = {3-540-14031-X},
  language = {USenglish},
  publisher = {Springer-Verlag},
  series = {LNCS 2646},
  title = {Using Theory Morphisms for Implementing Formal Methods Tools},
  year = 2003,
  classification = {workshop},
  user = {wolff}
}
@inproceedings{brucker.wolff:case,
  author = {Achim D. Brucker and Burkhart Wolff},
  title = {A Case Study of a Formalized Security Architecture},
  booktitle = {Eighth International Workshop onFormal Methods for
		  Industrial Critical Systems (FMICS'03)},
  volume = 80,
  classification = {workshop},
  editor = {Thomas Arts and Wan Fokkink},
  publisher = {Elsevier Science Publishers},
  year = 2003,
  language = {USenglish},
  abstract = {CVS is a widely known version management system, which can
		  be used for the distributed development of software as well
		  as its distribution from a central database.
		  
		  In this paper, we provide an outline of a formal security
		  analysis of a CVS-Server architecture performed
		  in~\cite{brucker.ea:cvs-server:2002}. The analysis is based
		  on an abstract architecture (enforcing a role-based access
		  control on the repository), which is refined to an
		  implementation architecture (based on the usual
		  discretionary access control provided by the \posix{}
		  environment). Both architectures serve as framework to
		  formulate access control and confidentiality properties.
		  
		  Both the abstract as well as the concrete architecture are
		  specified in the language Z. Based on a logical embedding
		  of Z into Isabelle/HOL, we provide formal, machine-checked
		  proofs for consistency properties of the specification, for
		  the correctness of the refinement, and for some security
		  properties.
		  
		  Thus, we present a case study for the security analysis of
		  realistic models over an off-the-shelf system by formal
		  machine-checked proofs. },
  pdf = {http://www.brucker.ch/bibliography/download/2003/fmics_03.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2003/fmics_03.ps.gz}
}
@article{brucker.rittinger.ea:hol-z,
  abstract = { We present a new proof environment for the specification
		  language Z. The basis is a semantic representation of Z in
		  a structure-preserving, shallow embedding in Isabelle/HOL.
		  On top of the embedding, new proof support for the Z schema
		  calculus and for proof structuring are developed. Thus, we
		  integrate Z into a well-known and trusted theorem prover
		  with advanced deduction technology such as higher-order
		  rewriting, tableaux-based provers and arithmetic decision
		  procedures. A further achievement of this work is the
		  integration of our embedding into a new tool-chain
		  providing a Z-oriented type checker, documentation
		  facilities and macro support for refinement proofs; as a
		  result, the gap has been closed between a logical embedding
		  proven correct and a \emph{tool} suited for applications of
		  non-trivial size.},
  author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  journal = {Journal of Universal Computer Science},
  classification = {journal},
  language = {USenglish},
  title = {{HOL-Z} 2.0: {A} {P}roof {E}nvironment for {Z}-{S}pecifications},
  volume = 9,
  year = 2003,
  number = 2,
  pages = {152--172},
  month = feb,
  issn = {0948-6968},
  ps = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.ps.gz},
  pdf = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.pdf},
  copyright = {\copyright J.UCS},
  doi = {10.3217/jucs-009-02-0152},
  copyrighturl = {http://www.jucs.org/jucs_9_2/hol_z_2}
}
@inproceedings{BCZ_msr03,
  author = {C. Besse and A. Cavalli and F. Za{\"i}di},
  title = {G{\'e}n{\'e}ration de tests d'interop{\'e}rabilit{\'e} pour le protocole TCP},
  booktitle = {4{\`e}me Colloque Francophone sur la Mod{\'e}lisation des Syst{\`e}mes R{\'e}actifs},
  year = 2003,
  address = {Metz},
  month = {October},
  publisher = {Herm{\`e}s}
}
@inproceedings{rauch.ea:formalizing:2003,
  abstract = {We present a formal model of the Java two's-complement
		  integral arithmetics. The model directly formalizes the
		  arithmetic operations as given in the Java Language
		  Specification (JLS). The algebraic properties of these
		  definitions are derived. Underspecifications and
		  ambiguities in the JLS are pointed out and clarified. The
		  theory is formally analyzed in Isabelle/HOL, that is,
		  machine-checked proofs for the ring properties and
		  divisor/remainder theorems etc. are provided. This work is
		  suited to build the framework for machine-supported
		  reasoning over arithmetic formulae in the context of Java
		  source-code verification.},
  author = {Nicole Rauch and Burkhart Wolff},
  booktitle = {Electronic Notes in Theoretical Computer Science},
  language = {USenglish},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2003/0_fmics03.pdf},
  classification = {workshop},
  publisher = {Elsevier Science Publishers},
  title = {Formalizing Java's Two's-Complement Integral Type in
		  Isabelle/HOL},
  volume = 80,
  year = 2003
}
@techreport{Go1364,
  author = {S.-D. Gouraud},
  title = {G\'en\'eration de Tests \`a l'Aide d'Outils
Combinatoires: Premiers R\'esultats Exp\'erimentaux},
  year = {2003},
  number = {1364},
  pdf = {\url{http//www.lri.fr/~gouraud/papiers/RR1364.pdf}}
}

2002

2002.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2002.bib -c 'year = 2002' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@techreport{platonis02,
  author = { Fatiha Za{\"i}di},
  title = {Mise en place du r{\'e}seau d'exp{\'e}rimentations},
  year = 2002,
  type = {Delivrable PLATONIS-FC-T13/D13},
  institution = {Institut National des T{\'e}l{\'e}communications, France}
}
@inproceedings{CMZ-sci02,
  author = {A. Cavalli and A. Mederreg and F. Za{\"i}di},
  title = {Mobiles Services Validation},
  booktitle = {The 6th World Conference on Systemics, Cybernics and Informatics},
  year = 2002,
  editor = {Nagib Callaos and al},
  address = {Orlando},
  month = {July},
  publisher = {IIIS}
}
@incollection{brucker.ea:hol-ocl:2002,
  title = {{HOL-OCL}: Experiences, Consequences and Design Choices},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2002},
  abstract = {Based on experiences gained from an embedding of the
		  Object Constraint Language (OCL) in higher-order
		  logic~\cite{brucker.ea:proposal:2002}, we explore several
		  key issues of the design of a formal semantics of the OCL.
		  These issues comprise the question of the interpretation of
		  invariants, pre- and postconditions, their transformation,
		  an executable sub-language and the possibilities of
		  refinement notions. A particular emphasize is put on the
		  issue of mechanized deduction in UML/OCL specification. },
  keywords = {OCL, Formal semantics, Constraint languages, Refinement,
		  higher-order logic},
  paddress = {Heidelberg},
  address = {Dresden},
  author = {Achim D. Brucker and Burkhart Wolff},
  classification = {conference},
  booktitle = {UML 2002: Model Engineering, Concepts and Tools},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/3-540-45800-X_17},
  language = {USenglish},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 2460,
  editor = {Jean-Marc J{\'e}z{\'e}quel and Heinrich Hussmann and
		  Stephen Cook},
  pdf = {http://www.brucker.ch/bibliography/download/2002/holocl_experiences.pdf},
  project = {CSFMDOS},
  year = 2002
}
@incollection{brucker.ea:proposal:2002,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-proposal-2002},
  abstract = {We present a formal semantics as a conservative shallow
		  embedding of the Object Constraint Language (OCL). OCL is
		  currently under development within an open standardization
		  process within the OMG; our work is an attempt to accompany
		  this process by a proposal solving open questions in a
		  consistent way and exploring alternatives of the language
		  design. Moreover, our encoding gives the foundation for
		  tool supported reasoning over OCL specifications, for
		  example as basis for test case generation.},
  keywords = {Isabelle, OCL, UML, shallow embedding, testing},
  paddress = {Heidelberg},
  address = {Hampton, VA, USA},
  author = {Achim D. Brucker and Burkhart Wolff},
  classification = {conference},
  booktitle = {Theorem Proving in Higher Order Logics},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/3-540-45685-6_8},
  editor = {C{\'e}sar Mu{\~n}oz and Sophi{\`e}ne Tahar and V{\'\i}ctor
		  Carre{\~n}o},
  language = {USenglish},
  pdf = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic.pdf},
  filelabel = {extended},
  file = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic_extended.pdf},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 2410,
  pages = {99--114},
  project = {CSFMDOS},
  title = {A Proposal for a Formal {OCL} Semantics in
		  {Isabelle/HOL}},
  year = 2002
}
@incollection{brucker.ea:cvs-server:2002,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002},
  author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  title = {The {CVS}-Server Case Study: A Formalized Security
		  Architecture},
  editor = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang
		  Reif},
  booktitle = {FM-TOOLS 2002},
  classification = {conference},
  year = 2002,
  series = {Technical Report},
  number = {2002--11},
  pages = {47--52},
  month = jul,
  organization = {University Augsburg},
  address = {Augsburg},
  pdf = {http://www.brucker.ch/bibliography/download/2002/fmtools_cvs_02.pdf},
  language = {USenglish},
  abstract = {CVS is a widely known version management system.
		  Configured in server mode, it can be used for the
		  distributed development of software as well as its
		  distribution from a central database called the
		  \emph{repository}. In this setting, a number of security
		  mechanisms have to be integrated into the CVS-server
		  architecture.
		  
		  We present an abstract formal model of the access control
		  aspects of a CVS-server architecture enforcing a role-based
		  access control on the data in the repository. This abstract
		  architecture is refined to an implementation architecture,
		  which represents (an abstraction of) a concrete CVS-server
		  configuration running in a POSIX/UNIX environment.
		  
		  Both the abstract as well as the concrete architecture are
		  specified in the language Z. The specification is compiled
		  to HOL-Z, such that refinement proofs for this case study
		  can be done in Isabelle/HOL. },
  project = {FSA}
}
@techreport{brucker.ea:cvs-server:2002-b,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002-b},
  author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  language = {USenglish},
  number = 182,
  title = {A {CVS-Server} Security Architecture --- Concepts and
		  Formal Analysis},
  abstract = {We present a secure architecture of a CVS-server, its
		  implementation (i.e. mainly its configuration) and its
		  formal analysis. Our CVS-server is uses cvsauth, that
		  provides protection of passwords and protection of some
		  internal data of the CVS repository. In contrast to other
		  (security oriented) CVS-architectures, our approach allows
		  the CVS-server run on an open filesystem, i.e. a filesystem
		  where users can have direct access both by CVS-commands and
		  by standard UNIX/POSIX commands such as \unixcmd{mv}.
		  
		  For our secure architecture of the CVS-server, we provide a
		  formal specification and security analysys. The latter is
		  based on a refinement mapping high-level security
		  requirements on the architecture on low-level security
		  mechanisms on the UNIX/POSIX filesystem level.
		  
		  The purpose of the formal analysis of the secure CVS-server
		  architecture is twofold: First, it is the bases for the
		  specification of mutual security properties such as
		  non-repudiation, authentication and access control for this
		  architecture. Second, the mapping of the architecture on
		  standard security implementation technology is described.
		  
		  Thus, our approach can be seen as a method to give a formal
		  underpinning for the usually tricky business of system
		  administrators.},
  keywords = {security architecture, Concurrent Versions System (CVS),
		  Z, formal methods, refinement},
  year = 2002,
  classification = {unrefereed},
  num_pages = 100,
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2002/cvs_arch.pdf},
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2002/cvs_arch.ps.gz}
}
@incollection{brucker.ea:hol-z:2002,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-z-2002},
  author = {Achim D. Brucker and Stefan Friedrich and Frank Rittinger
		  and Burkhart Wolff},
  title = {{HOL}-{Z} 2.0: A Proof Environment for Z-Specifications},
  editor = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang
		  Reif},
  booktitle = {FMTOOLS 2002},
  classification = {conference},
  year = 2002,
  series = {Technical Report},
  pages = {33--38},
  month = jul,
  number = {2002--11},
  organization = {University Augsburg},
  address = {Augsburg},
  pdf = {http://www.brucker.ch/bibliography/download/2002/fmtools_holz_02.pdf},
  language = {USenglish},
  abstract = {We present a proof environment for the specification
		  language Z on top of Isabelle/HOL. It comprises a
		  \LaTeX-based front end (including the integrated
		  type-checker ZETA), generic facilities to generate proof
		  obligations and improved proof support for the logical
		  embedding HOL-Z, namely for the schema-calculus and
		  structural Z proofs. },
  project = {FSA}
}
@techreport{wolff:ea:mixe:2002,
  author = {Burkhart Wolff and Oliver Berthold and Sebastian Clau{\ss}
		  and Hannes Federrath and Stefan K{\"o}psell and Andreas
		  Pfitzmann},
  title = {Towards a Formal Analysis of a Mix Network},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  year = 2002,
  series = {Technical Report},
  number = 171,
  issn = 14341719,
  pdf = {2003/tr01.pdf},
  language = {USEnglish},
  classification = {unrefereed}
}
@inproceedings{testcom02,
  author = {C{\'e}dric Besse and Ana R. Cavalli and Myungchul Kim and Fatiha Za\"{\i}di},
  title = {Automated Generation of Interoperability Tests},
  booktitle = {FIP/TC6/WG6.1 Fourteenth International Conference on Testing of Communicating Systems (Testcom 2002)},
  year = {2002},
  address = {Berlin},
  month = {March},
  note = {ISBN 0-7923-7695-1},
  pages = {169-184},
  publisher = {Kluwer Academic}
}
@inproceedings{LG02,
  author = {G. Lestiennes and M.-C. Gaudel},
  title = {Testing processes from formal specifications with inputs, outputs, and datatypes},
  booktitle = {IEEE Int. Symp. on Software Reliability Engineering (ISSRE)},
  year = {2002},
  pages = {3-14},
  pdf = {http://www.lri.fr/~mcg/PDF/LesGau02.pdf}
}

2001

2001.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2001.bib -c 'year = 2001' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@techreport{castor01,
  author = { Fatiha Za{\"i}di},
  title = {Test du Service RPVM},
  year = 2001,
  type = {Delivrable FC-T222},
  institution = {Institut National des T{\'e}l{\'e}communications, France}
}
@inproceedings{CDRZ-ISCC01,
  author = {A. Cavalli and B. Defude and Ch. Rinderknecht and F. Za{\"i}di},
  title = {A {S}ervice-{C}omponent {T}esting {Method} adn {S}uitable {CORBA} {A}rchitecture},
  booktitle = {Proceedings of the Sixth {IEEE} Symposium on Computers and Communications},
  pages = {655--660},
  year = 2001,
  editor = {IEEE Computer Society},
  address = {Tunisia},
  month = {July}
}
@techreport{brucker.ea:checking:2001,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-checking-2001},
  author = {Achim D. Brucker and Burkhart Wolff},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  language = {USenglish},
  month = jul,
  classification = {unrefereed},
  title = {{Checking OCL Constraints in Distributed Systems Using
		  J2EE/EJB}},
  abstract = {We present a pragmatic approach using formal methods to
		  increase the quality of distributed component based
		  systems: Based on UML class diagrams annotated with OCL
		  constraints, code for runtime checking of components in
		  J2EE/EJB is automatically generated. Thus, a UML--model for
		  a component can be used in a black--box test for the
		  component. Further we introduce different design patterns
		  for EJBs, which are motivated by different levels of
		  abstraction, and show that these patterns work smoothly
		  together with our OCL constraint checking.
		  
		  A prototypic implementation of the code generator,
		  supporting our design patterns with OCL support, has been
		  integrated into a commercial software development tool.},
  keywords = {OCL, Constraint checking, EJB, J2EE, Design by Contract,
		  Design Pattern, Distributed Systems},
  year = 2001,
  number = 157,
  num_pages = 46,
  contributions = {Using OCL Constrains in a EJB environment and Design
		  Patterns for EJBs.},
  pdf = {http://www.brucker.ch/bibliography/download/2001/tr01.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2001/tr01.ps.gz}
}
@inproceedings{brucker.ea:testing:2001,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-testing-2001},
  author = {Achim D. Brucker and Burkhart Wolff},
  classification = {proceedings},
  title = {Testing Distributed Component Based Systems Using
		  {UML/OCL}},
  language = {USenglish},
  booktitle = {Informatik 2001},
  pages = {608--614},
  year = 2001,
  editor = {K. Bauknecht and W. Brauer and Th. M{\"u}ck},
  volume = 1,
  number = 157,
  series = {Tagungsband der GI/{\"O}CG Jahrestagung},
  address = {Wien},
  month = nov,
  organization = {{\"O}sterreichische Computer Gesellschaft},
  abstract = {We present a pragmatic approach using formal methods to
		  increase the quality of distributed component based
		  systems: Based on UML class diagrams annotated with OCL
		  constraints, code for runtime checking of components in
		  J2EE/EJB is automatically generated. Thus, a UML--model for
		  a component can be used in a black--box test for the
		  component. Further we introduce different design patterns
		  for EJBs, which are motivated by different levels of
		  abstraction, and show that these patterns work smoothly
		  together with our OCL constraint checking.
		  
		  A prototypic implementation of the code generator,
		  supporting our patterns with OCL support, has been
		  integrated into a commercial software development tool.},
  isbn = {3-85403-157-2},
  pdf = {http://www.brucker.ch/bibliography/download/2001/info2001.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2001/info2001.ps.gz}
}
@inproceedings{wolff:verifying:2001,
  abstract = {Binding structures enrich traditional abstract syntax by
		  provi-ding support for representing binding mechanisms
		  (based on deBruijn indices), term-schemata and a very clean
		  algebraic theory of substitution. Weprovide a novel binding
		  structure with the following main results: 1) The
		  formalisation of a generic binding structure with the novel
		  conceptof effect-binding that enables the explicit
		  representations of both contexts and terms inside one term
		  meta-language,2) The foundation of a formal
		  (machine-assisted) substitution theory of effect-binding
		  that is well-suited for mechanisation. This can be used for
		  thesystematic and correct development of new calculi with
		  explicit substitutions.The substitution theory is formally
		  proven in Isabelle/HOL; the implementation may serve as
		  (untyped) framework for deep embeddings.},
  author = {Burkhart Wolff},
  classification = {proceedings},
  booktitle = {Workshop on Explicit Substitution Theory and Applications
		  (WESTAPP'01)},
  editor = {Pierre Lescanne},
  isbn = {90-393-2764-5},
  language = {english},
  month = {May},
  pages = {58 -- 71},
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2001/BiSE.ps.gz},
  publisher = {Department of Philosophy - Utrecht University},
  series = {Logic Group Preprint Series},
  title = {Verifying Explicit Substitution Calculi in Binding
		  Structures with Effect Binding},
  classification = {workshop},
  volume = 210,
  year = 2001
}
@techreport{luth.ea:smltk:2001,
  abstract = {In this reference manual, we describe the SML-based
		  programming environment sml_tk for graphical user
		  interfaces, version 3.0. sml_tk is based on the highly
		  portable X-Window Toolkit Tk (and uses internally the
		  Tcl/Tk interpreter wish), but offers functional abstraction
		  over Tk and an own component library for graphical standard
		  widgets such as info-boxes, treelist-widgets, tabs and
		  tables. sml_tk is the basic library for a collection of
		  GUIs for formal method tools such as TAS and IsaWin.},
  author = {Christoph L{\"u}th and Burkhart Wolff},
  classification = {unrefereed},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  language = {english},
  month = {July},
  number = 158,
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2001/manual.pdf},
  title = {sml\_tk: Functional Programming for GUIs -- Reference
		  Manual},
  year = 2001
}
@misc{campinas,
  author = {F. Za{\"i}di},
  title = { Open Problems in protocol testing},
  howpublished = {Workshop on protocol and dsitributed systems testing},
  month = {October},
  year = 2001,
  note = { Universit{\'e} de Campinas, Br{\'e}sil}
}
@inproceedings{Ada2001,
  author = {Gaudel, Marie-Claude},
  affiliation = {Universit de Paris-Sud et CNRS L.R.I Bt. 490 F-91405 Orsay-cedex France},
  title = {Testing from Formal Specifications, a Generic Approach},
  booktitle = {Reliable SoftwareTechnologies  Ada-Europe 2001},
  series = {Lecture Notes in Computer Science},
  editor = {Craeynest, Dirk and Strohmeier, Alfred},
  publisher = {Springer Berlin / Heidelberg},
  pages = {35-48},
  volume = {2043},
  note = {invited lecture},
  year = {2001}
}
@inproceedings{Go01,
  author = {S.-D. Gouraud},
  title = {Application de la G\'en\'eration Al\'eatoire de Structures Combinatoires au Test de Logiciel},
  booktitle = {Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels (AFADL)},
  pages = {99-112},
  year = {2001},
  pdf = {http://www.lri.fr/~gouraud/papers/Go01.pdf},
  type_digiteo = {conf_autre}
}
@inproceedings{GoDeGaMa01,
  author = {S.-D. Gouraud and A. Denise and M.-C. Gaudel and B. Marre},
  title = {A new way of automating Statistical Testing Methods },
  booktitle = {16th. IEEE International Conference on Automated Software Engineering (ASE)},
  year = {2001},
  pages = {5-12},
  type_digiteo = {conf_isbn},
  pdf = {http://www.lri.fr/~gouraud/papers/GoDeGaMa01.pdf}
}
@techreport{GoDeGaMa1290,
  author = {S.-D. Gouraud and A. Denise and M.-C. Gaudel and B. Marre},
  title = {A New Way of Automating Statistical Testing Methods},
  year = {2001},
  number = {1290}
}
@inproceedings{ase2001,
  author = {S.-D. Gouraud and A. Denise and M.-C. Gaudel and B. Marre},
  title = {A New Way of Automating Statistical Testing Methods},
  booktitle = {IEEE International Conference on Automated Software Engineering (ASE)},
  year = {2001},
  pages = {5-12},
  pdf = {http://www.lri.fr/~mcg/PDF/ase2001Revise.pdf}
}

2000

2000.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/2000.bib -c 'year = 2000' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{cfip00,
  author = {A. Cavalli and B. Defude  and Ch. Rinderknecht and F. Za{\"i}di},
  title = {Test de composants de service et ex{\'e}cution de tests sur une plateforme CORBA},
  booktitle = {CFIP'2000 Ing{\'e}nierie des protocoles},
  pages = {363-378},
  year = 2000,
  editor = {Patrick S{\'e}nac Jean-Pierre Courtiat, Michel Diaz},
  address = {Toulouse},
  month = {October},
  publisher = {Herm{\`e}s}
}
@inproceedings{luth.ea:more:2000,
  author = {Christoph L{\"u}th and Burkhart Wolff},
  title = {More about {TAS} and {IsaWin}: Tools for Formal Program
		  Development},
  editor = {T. Maibaum},
  booktitle = {Fundamental Approaches to Software Engineering {FASE 2000}.
		  Joint European Conferences on Theory and Practice of
		  Software {ETAPS 2000}},
  year = 2000,
  language = {USenglish},
  classification = {conference},
  series = {Lecture Notes in Computer Science},
  pages = {367-- 370},
  publisher = {Springer Verlag},
  number = 1783,
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/sysdesc.ps.gz},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/sysdesc.pdf.gz},
  abstract = {We present a family of tools for program development and
		  verification, compris\- ing the transformation system TAS
		  and the theorem proving interface IsaWin. Both are based on
		  the theorem prover Isabelle, which is used as a generic
		  logical framework here. A graphical user interface, based
		  on the principle of di\- rect manipulation, allows the user
		  to interact with the tool without having to concern himself
		  with the details of the representation within the theorem
		  prover, leaving him to concentrate on the main design
		  decisions of program development or theorem proving. The
		  tools form an integrated system for formal program
		  development, in which TAS is used for transformational
		  program development, and IsaWin for discharging the
		  incurred proof obligations. However, both tools can be used
		  sep\- arately as well. Further, the tools are generic over
		  the formal method employed. In this extended abstract, we
		  will first give a brief overview over TAS and IsaWin. Since
		  TAS and IsaWin have been presented on previous ETAPS
		  conferences, the presentation will highlight the new
		  features as sketched out below. }
}
@inproceedings{luth.ea:tas:2000,
  author = {Christoph L{\"u}th and Burkhart Wolff},
  title = {{TAS} --- A Generic Window Inference System},
  editor = {J. Harrison and M. Aagaard},
  booktitle = {Theorem Proving in Higher Order Logics: 13th International
		  Conference, TPHOLs 2000},
  year = 2000,
  classification = {conference},
  series = {Lecture Notes in Computer Science},
  pages = {405--422},
  publisher = {Springer Verlag},
  number = 1869,
  pdf = {http://www.lri.fr/~wolff/papers/conf/TAS-tphols00.pdf},
  language = {USenglish},
  abstract = {This paper presents work on technology for
		  transformational proof and program development, as used by
		  window inference calculi and transformation systems. The
		  calculi are characterised by a certain class of theorems in
		  the underlying logic. Our transformation system TAS
		  compiles these rules to concrete deduction support,
		  complete with a graphical user interface with
		  command-language-free user interaction by gestures like
		  drag&drop and proof-by-pointing, and a development
		  management for transformational proofs. It is
		  generic in the sense that it is completely
		  independent of the particular window inference or
		  transformational calculus, and can be instantiated to many
		  different ones; three such instantiations are presented in
		  the paper.}
}
@article{basin.ea:berichte:2000,
  author = {David Basin and Luca Vigan{\`o} and Burkhart Wolff},
  classification = {conference},
  file = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/overview.ps.gz},
  filelabel = {English translation},
  journal = {PIK (Praxis der Informationsverarbeitung und
		  Kommunikation)},
  language = {german},
  number = 4,
  pages = {248--249},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/uebersicht.pdf},
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/uebersicht.ps.gz},
  title = {Berichte aus den Instituten: Lehrstuhl f{\"u}r
		  Softwaretechnik und Softwareproduktionsumgebung, Freiburg},
  volume = 23,
  year = 2000
}
@misc{snpd,
  author = {F. Za{\"i}di and A. Cavalli},
  title = {Tutorial: Automatic embedded test generation. Universit{\'e} de Reims},
  howpublished = {International Conference on Software Engineering Applied to Networking and Parallel/Distributed Computing (SNPD'2000)},
  month = {May},
  year = 2000
}
@masterthesis{Gouraud00,
  author = {S.-D. Gouraud},
  title = {Application
des Techniques de G\'en\'eration Al\'eatoire au Test de
Logiciel},
  school = {Universit\'e Paris-Sud 11, LRI},
  year = {2000},
  pdf = {http://www.lri.fr/~gouraud/papers/dea_gouraud.pdf}
}
@inproceedings{meyer.ea:correct:2000,
  author = {T. Meyer and Burkhart Wolff},
  title = {Correct Code-Generation in a Generic Framework},
  editor = {M. Aargaard and J. Harrison and T. Schubert},
  classification = {workshop},
  booktitle = {TPHOLs 2000: Supplemental Proceedings},
  year = 2000,
  series = {OGI Technical Report CSE 00-009},
  pages = {213--230},
  month = jul,
  organization = {Oregon Graduate Institute, Portland, USA},
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/CodeGen.ps.gz},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2000/CodeGen.pdf},
  language = {USenglish},
  abstract = {One major motivation for theorem provers is the
		  development of verified programs. In particular, synthesis
		  or transformational development techniques aim at a
		  formalised conversion of the original specification to a
		  final formula meeting some notion of executability. We
		  present a framework to describe such notions, a method to
		  formally investigate them and instantiate it for three
		  executable languages, based on three different forms of
		  recursion (two denotational and one based on well-founded
		  recursion) and develop their theory in Isabelle/HOL. These
		  theories serve as a semantic interface for a generic
		  code-generator which is set up for each program notion with
		  an individual code-scheme for SML.}
}

1999

1999.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1999.bib -c 'year = 1999' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{algo-sirius,
  author = {A. Cavalli and D. Lee and C. Rinderknecht and F. Za{\"i}di},
  title = {Hit-or-{J}ump: {A}n algorithm for {E}mbedded {T}esting with {A}pplications to {I}n {S}ervices},
  booktitle = {Proceeding of {IFIP} {I}nternational conference {FORTE}/{PSTV}'99},
  year = {1999},
  editor = {Jianping Wu and al.},
  pages = {41-56},
  address = {Beijing, China},
  month = {October}
}
@inproceedings{jdir,
  author = {Ana Cavalli and David Lee and Christian Rinderknecht and Fatiha Za{\"i}di},
  title = {Un algorithme pour le test imbriqu{\'e} avec des applications aux services R.I},
  booktitle = {Actes de la 3{\`e}me {\'e}dition des journ{\'e}es Doctorales Informatique et R{\'e}seaux},
  pages = {22-24},
  year = 1999,
  address = {Insitut National des T{\'e}l{\'e}communications, Evry},
  month = {November}
}
@article{luth.ea:functional:1999,
  author = {Christoph L{\"u}th and Burkhart Wolff},
  title = {Functional Design and Implementation of Graphical User
		  Interfaces for Theorem Provers},
  journal = {Journal of Functional Programming},
  year = 1999,
  volume = 9,
  number = 2,
  pages = {167-- 189},
  classification = {journal},
  doi = {10.1017/S0956796899003421},
  month = march,
  abstract = {This paper attempts to develop a metaphor suited to
		  visualize the LCF-style prover design, and a methodology
		  for the implementation of graphical user interfaces for
		  these provers and encapsulations of formal methods. In this
		  problem domain, particular attention has to be paid to the
		  need to construct a variety of objects, keep track of their
		  interdependencies and provide support for their
		  reconstruction as a consequence of changes. We present a
		  prototypical implementation of a generic and
		  open interface system architecture, and show how
		  it can be instantiated to an interface for Isabelle, called
		  IsaWin, as well as to a tailored tool for transformational
		  program development, called TAS.},
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/1999/fungui.ps.gz},
  language = {USenglish},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/1999/fungui.pdf}
}
@article{JEG99,
  author = {P. R. James and M. Endler and
               M.-C. Gaudel},
  title = {Development of an Atomic Broadcast Protocol using {LOTOS}},
  journal = {Software Practice and Experience},
  year = {1999},
  volume = {29},
  number = {8},
  pages = {699-719},
  comment = {no file available}
}

1998

1998.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1998.bib -c 'year = 1998' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{lwkww98a,
  author = {C. L{\"u}th and E. W. Karlsen and Kolyang and S. Westmeier
		  and B. Wolff},
  booktitle = {Workshop on Tool Support for System Specification,
		  Development, and Verification},
  editor = {Berghammer and Hoffmann},
  title = {Tool integration in the UniForM Workbench},
  year = 1998,
  ps = {1998/tools.ps.gz},
  language = {USEnglish},
  abstract = {The UniForM-Workbench is an open tool-integration
		  environment providing type-safe communication, a toolkit
		  for graphical user-interfaces, version management and
		  configuration management. We demonstrate how to integrate
		  several tools for the Z specification language into the
		  workbench, obtaining an instantiation of the workbench
		  suited as a software development environment for Z. In the
		  core of the setting, we use the encoding HOL-Z of Z into
		  Isabelle as semantic foundation and for formal reasoning
		  with Z specifications. In addition to this, external tools
		  like editors and small utilities are integrated, showing
		  the integration of both self-developed and externally
		  developed tools. The resulting prototype demonstrates the
		  viability of our approach to combine public domain tools
		  into a generic software development environment using a
		  strongly typed functional language. },
  classification = {workshop}
}
@inproceedings{luth.ea:hol-z:1998,
  author = {Chritoph L{\"u}th and Einar W. Karlsen and Kolyang and
		  Stefan Westmeier and Burkhart Wolff},
  classification = {conference},
  booktitle = {11. International Conference of Z Users ZUM'98},
  editor = {J. Bowen},
  pages = {116--134},
  publisher = {Springer Verlag},
  series = {LNCS 1493},
  title = {{HOL-Z} in the {UniForM-Workbench} -- a Case Study in Tool
		  Integration for Z},
  year = 1998,
  doi = {10.1007/BFb0056029},
  ps = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/1998/zinuniform.ps.gz},
  abstract = {The UniForM-Workbench is an open tool-integration
		  environment providing type-safe communication, a toolkit
		  for graphical user-interfaces, version management and
		  configuration management. We demonstrate how to integrate
		  several tools for the Z specification language into the
		  workbench, obtaining an instantiation of the workbench
		  suited as a software development environment for Z. In the
		  core of the setting, we use the encoding HOL-Z of Z into
		  Isabelle as semantic foundation and for formal reasoning
		  with Z specifications. In addition to this, external tools
		  like editors and small utilities are integrated, showing
		  the integration of both self-developed and externally
		  developed tools. The resulting prototype demonstrates the
		  viability of our approach to combine public domain tools
		  into a generic software development environment using a
		  strongly typed functional language. }
}
@article{GJ98,
  author = {M.-C. Gaudel and P. R. James},
  title = {Testing Algebraic Data Types and Processes: a unifying theory},
  journal = {Formal Aspects of Computing},
  volume = {10(5-6)},
  pages = {436--451},
  year = {1998},
  pdf = {http://www.lri.fr/~mcg/PDF/GJ99.pdf}
}

1997

1997.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1997.bib -c 'year = 1997' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@phdthesis{wolff97,
  author = {B. Wolff},
  title = {A Generic Calculus of Transformations},
  school = {Universit{\"a}t Bremen},
  pubisher = {Shaker-Verlag},
  address = {Aachen},
  isbn = {3-8265-3654-1},
  year = 1997,
  ps = {1997/diss.tar.gz},
  language = {USEnglish},
  abstract = {\textbf{Binding structures} enrich traditional abstract
		  syntax by providing support for representing binding
		  mechanisms (based on deBruijn indices), term-schemata and a
		  very clean algebraic theory of substitution. We provide the
		  following main results: \begin{itemize} \item The
		  establishment of a \emph{generic} binding structure with
		  the novel concept of effect-binding that enables the
		  representations of both signatures and formulas (i.e.
		  specifications) inside one term meta- language, \item The
		  foundation of a formal (machine-assisted) substitution
		  theory of effect-binding that is well-suited for
		  mechanisation. This may contribute to the construction of
		  tools such as theorem provers, program transformers, static
		  analysers, evaluators and optimising compilers, \item The
		  foundation of a rigorous meta-theory for rewriting on
		  effect- binding-structures. The resulting rewrite notion
		  transformation extends combinatory rewrite systems to
		  rewrites on specifications. \end{itemize} The corner stone
		  of this theory is a confluence proof for orthogonal
		  transformations (partly implemented in the proof assistant
		  Isabelle). },
  classification = {book}
}
@inproceedings{tw97,
  author = {H. Tej and B. Wolff},
  booktitle = {Proceedings of the FME 97 --- Industrial Applications and
		  Strengthened Foundations of Formal Methods},
  editor = {J. Fitzgerald and C.B. Jones and P. Lucas},
  pages = {318--337},
  publisher = {Springer Verlag},
  series = {LNCS 1313},
  title = {A Corrected Failure-Divergence Model for CSP in
		  Isabelle/HOL},
  year = 1997,
  ps = {1997/CSP.ps.gz},
  pdf = {1997/CSP.pdf},
  language = {USEnglish},
  doi = {10.1007/3-540-63533-5_17},
  abstract = {We present a failure-divergence model for CSP following
		  the concepts of [BR 85]. Its formal representation within
		  higher order logic in the theorem prover Isabelle/HOL [Pau
		  94] revealed an error in the basic definition of CSP
		  concerning the treatment of the termination symbol tick. A
		  corrected model has been formally proven consistent with
		  Isabelle HOL. Moreover, the changed version maintains the
		  essential algebraic properties of CSP. As a result, there
		  is a proven correct implementation of a ``CSP
		  workbench{\'{}}{\'{}} within Isabelle. },
  classification = {conference}
}
@inproceedings{klmw97,
  author = {Kolyang and C. L{\"u}th and T. Meier and B. Wolff},
  booktitle = {TAPSOFT 97: Theory and Practice of Software Development },
  editor = {M. Bidoit, M. Dauchet},
  pages = {855--858},
  publisher = {Springer Verlag},
  series = {LNCS 1214},
  doi = {10.1007/BFb0030646},
  title = {TAS and IsaWin: Generic Interfaces for Transformational
		  Program Development and Theorem Proving},
  year = 1997,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/tapsoft.ps.gz},
  language = {USEnglish},
  classification = {conference}
}
@inproceedings{klmw97b,
  author = {Kolyang and C. L{\"}uth and T. Meier and B. Wolff},
  booktitle = {Proceedings of the ``International Workshop for Tool
		  Support in Verification and Validation{\'{}}{\'{}}},
  editor = {K.Berghammer, J.Peleska, B. Buth},
  publisher = {Shaker Verlag},
  series = {BISS Monographs},
  title = {Generic Interfaces for Transformation Systems and
		  Interactive Theorem Provers. },
  year = 1997,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/tsv.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}

1996

1996.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1996.bib -c 'year = 1996' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@techreport{lww96,
  author = {C. L{\"u}th and S. Westmeier and B. Wolff},
  institution = {Universit{\"a}t Bremen},
  title = {sml_tk: Functional Programming for Graphical User
		  Interfaces},
  number = {8/96},
  year = 1996,
  comment = {outdated version 2.1},
  ps = {http://www.informatik.uni-bremen.de/~cxl/sml_tk/doc/Titel.ps.gz;
		  http://www.informatik.uni-bremen.de/~cxl/sml_tk/doc/DOC.ps.gz},
  language = {USEnglish},
  classification = {unrefereed}
}
@inproceedings{klmw96a,
  author = {Kolyang and C. L{\"u}th and T. Meier and B. Wolff},
  booktitle = {Proceedings of the User Interfaces for Theorem Provers
		  (UITP 96)},
  editor = {N. Merriam},
  publisher = {University of York},
  series = {Technical Report},
  title = {Generating Graphical User-Interfaces in a Functional
		  Setting},
  year = 1996,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/uitp96.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}
@inproceedings{ksw96a,
  author = {Kolyang and T. Santen and B. Wolff},
  booktitle = {FME 96 --- Industrial Benefits and Advances in Formal
		  Methods},
  editor = {M.-C. Gaudel and J. Woodcock},
  pages = {629--648},
  publisher = {Springer Verlag},
  series = {LNCS 1051},
  title = {Correct and User-Friendly Implementation of Transformation
		  Systems},
  year = 1996,
  abstract = {We present an approach to integrate several existing tools
		  and methods to a technical framework for correctly
		  developing and executing program transformations. The
		  resulting systems enable program derivations in a
		  user-friendly way. We illustrate the approach by proving
		  and implementing the transformation Global Search on the
		  basis of the tactical theorem prover Isabelle. A graphical
		  user-interface based on the X-Window toolkit Tk provides
		  user friendly access to the underlying machinery.},
  ps = {1996/yats.ps.gz},
  pdf = {1996/yats.pdf},
  language = {USEnglish},
  doi = {10.1007/3-540-60973-3_111},
  classification = {conference}
}
@inproceedings{ksw96b,
  author = {Kolyang and T. Santen and B. Wolff},
  booktitle = {Theorem Proving in Higher Order Logics --- 9th
		  International Conference},
  editor = {J. von Wright and J. Grundy and J. Harrison},
  pages = {283--298},
  publisher = {Springer Verlag},
  series = {LNCS 1125},
  title = {A Structure Preserving Encoding of Z in Isabelle/HOL},
  year = 1996,
  comment = {The distributed version is slightly corrected w.r.t. the
		  original one.},
  ps = {1996/SPEZ_HOL.R.23.ps.gz},
  pdf = {1996/SPEZ_HOL.R.23.pdf},
  language = {USEnglish},
  abstract = {We present a semantic representation of the core concepts
		  of the specification language Z in higher-order logic.
		  Although it is a ``shallow embedding{\'{}}{\'{}} like the
		  one presented by Bowen and Gordon, our representation
		  preserves the structure of a Z specification and avoids
		  expanding Z schemas. The representation is implemented in
		  the higher- order logic instance of the generic theorem
		  prover Isabelle. Its parser can convert the concrete syntax
		  of Z schemas into their semantic representation and thus
		  spare users from having to deal with the representation
		  explicitly. Our representation essentially conforms with
		  the latest draft of the Z standard and may give both a
		  clearer understanding of Z schemas and inspire the
		  development of proof calculi for Z.},
  classification = {conference}
}
@incollection{boiler,
  author = {M.-C. Gaudel and P. Dauchy and C. Khoury},
  booktitle = {Formal Methods for Industrial Applications: specifying and programming the Steam Boiler Control},
  title = {A Formal Specification of the Steam-Boiler Control Problem by Algebraic Specifications with Implicit State},
  publisher = {Springer-Verlag},
  volume = 1165,
  series = {Lecture Notes in Computer Science},
  year = {1996},
  pages = {233-264},
  pdf = {http://www.lri.fr/~mcg/PDF/Boiler-fulltext.pdf}
}

1995

1995.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1995.bib -c 'year = 1995' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{Transit,
  author = {A. Arnold and M. Gaudel and B. Marre},
  title = {An Experiment on the Validation of a Specification by Heterogeneous Formal
    Means: The Transit Node},
  booktitle = { 5th IFIP Working Conference on Dependable Computing for Critical Applications
    (DCCA5)},
  pages = {24--34},
  year = {1995},
  comment = {file to be found}
}
@inproceedings{klsw95,
  author = {B. Krieg-Br{\"u}ckner and J. Liu and H. Shi and B. Wolff},
  booktitle = {KORSO --- Methods, Languages, and Tools for the
		  Construction of Correct Software},
  editor = {M. Broy and S. J{\"a}hnichen},
  pages = {270--284},
  publisher = {Springer Verlag},
  series = {LNCS 1009},
  title = {Towards Correct, Efficient and Re-usable Transformational
		  Developments},
  year = 1995,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/klsw37.kurz.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}
@inproceedings{Gaudel95,
  author = {Gaudel, M.-C.},
  title = {Testing can be formal, too},
  booktitle = {TAPSOFT'95, International Joint Conference, Theory
		  And Practice of Software Development},
  publisher = {Springer Verlag},
  volume = 915,
  series = {Lecture Notes in Computer Science},
  year = 1995,
  address = {Aarhus, Denmark},
  pages = {82-96},
  pdf = {http://www.lri.fr/~mcg/PDF/TAPSOFTfin.pdf}
}
@inproceedings{kw95,
  author = {Kolyang and B. Wolff},
  booktitle = {Beitr{\"a}ge der GI-Fachtagung ``Softwaretechnik
		  95{\'{}}{\'{}}, Braunschweig},
  editor = {G. Snelting},
  pages = {57--66},
  publisher = {GI},
  series = {Mitteilungen der Fachgruppen `Software Engineering{\'{}}
		  und `Requirements-Engineering{\'{}},Band 15, Heft 3, ISSN
		  0720-8928},
  title = {Development by Refinement Revisited: Lessons learnt from
		  an example.},
  year = {1995},
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/LEX.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}

1993

1993.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1993.bib -c 'year = 1993' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@article{DGM93,
  author = {P. Dauchy and M.-C. Gaudel and B. Marre},
  title = {Using Algebraic Specifications in Software Testing : a case study on the software of an automatic subway},
  journal = {Journal of Systems and Software},
  year = {1993},
  volume = {21},
  number = {3},
  pages = {229-244},
  pdf = {http://www.lri.fr/~mcg/PDF/jss93.pdf}
}

1992

1992.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1992.bib -c 'year = 1992' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{BGM92,
  author = {G. Bernot and M.-C. Gaudel and B. Marre},
  title = {A Formal Approach to Software Testing},
  booktitle = {2nd International Conference on Algebraic Methodology and Software Technology (AMAST)},
  number = 670,
  series = {Worshops in Computing Series},
  year = 1992,
  pages = {243-253},
  publisher = {Springer Verlag},
  pdf = {http://www.lri.fr/~mcg/PDF/amast93.pdf}
}

1991

1991.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1991.bib -c 'year = 1991' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@article{BGM91,
  author = {G. Bernot and
               M.-C. Gaudel and
               B. Marre},
  title = {Software testing based on formal specifications: a theory and a tool},
  journal = {Software Engineering Journal},
  year = {1991},
  volume = {6},
  number = {6},
  pages = {387-405},
  pdf = {http://www.lri.fr/~mcg/PDF/sej91.pdf}
}

1986

1986.bib

@comment{{This file has been generated by bib2bib 1.94}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/1986.bib -c 'year = 1986' -s author /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/poizat/WWW/poizat.bib /users/asspro/zaidi/WWW/zaidi.bib /users/asspro/wolff/WWW/bibtex/wolff.bib /users/asspro/longuet/WWW/longuet.bib /users/asspro/wenzel/WWW/papers/wenzel.bib /users/asspro/feliachi/WWW/feliachi.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib /users/asspro/zaidi/WWW/zaidi.bib zaidi_from_wiki.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -c 'author : "Zaidi"' /users/asspro/zaidi/Plan-quadriennal/Plan-quadriannual/publi0508fortesse.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{modifications en dur par MCG}}
@comment{{Command line: /usr/bin/bib2bib -ob fortesse.bib -c year>=2005 /users/asspro/gouraud/WWW/gouraud.bib /users/asspro/mcg/WWW/mcg.bib /users/asspro/oudinet/WWW/oudinet.bib /users/asspro/zaidi/WWW/zaidi.bib /tmp/fayolleAPRES.bib}}
@comment{{This file has been generated by bib2bib 1.88}}
@comment{{Command line: /usr/bin/bib2bib -ob /tmp/fayolleAPRES.bib -c year>=2007 /users/asspro/fayolle/WWW/fayolle.bib}}
@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@article{Boug86,
  author = {L. Boug\'e and N.Choquet and L. Fribourg and M.-C. Gaudel},
  title = {Test set generation from algebraic specifications using logic programming},
  journal = {Journal of Systems and Software},
  year = {1986},
  volume = {6},
  number = {4},
  pages = {343-360},
  comment = {no file}
}
Design created by Johan Oudinet