ForTesSE Group

Achim D Brucker, Lukas Brügger and Burkhart Wolff. Formal Firewall Testing: An Application of Test and Proof Techniques. Softw. Test., Verif. Reliab. 25(1):34–71, 2015.
[ BibTeX | pdf ]

@article{brucker-wolff:FormalFirewallTest:2013,
	author = {Achim D. Brucker and Lukas Br\"ugger and Burkhart Wolff},
	title = "Formal Firewall Testing: An Application of Test and Proof Techniques",
	journal = "Softw. Test., Verif. Reliab.",
	volume = 25,
	number = 1,
	year = 2015,
	pages = "34--71",
	abstract = "Firewalls are an important means to secure critical ICT infrastructures. As configurable off-the-shelf products, the effectiveness of a firewall crucially depends on both the correctness of the implementation itself as well as the correct configuration. While testing the implementation can be done once by the manufacturer, the configuration needs to be tested for each application individually. This is particularly challenging as the configuration, implementing a firewall policy, is inherently complex, hard to understand, administrated by different stakeholders and, thus, difficult to validate. This paper presents a formal model of both stateless and stateful firewalls (packet filters), including network address translation (NAT), to which a specification-based conformance test case generation approach is applied. Furthermore, a verified optimisation technique for this approach is presented: Starting from a formal model for stateless firewalls, a collection of semantics-preserving policy transformation rules and an algorithm that optimises the specification with respect of the number of test cases required for path coverage of the model are derived. We extend an existing approach that integrates verification and testing, i. e., tests and proofs to support conformance testing of network policies. The presented approach is supported by a test framework that allows to test actual firewalls using the test cases generated based on the formal model. Finally, a report on several larger case studies is presented.",
	pdf = "https://www.lri.fr/~wolff/papers/journals/2010-stvr-fw-test.pdf",
	doi = "10.1002/stvr.1544"
}

Delphine Longuet, Frédéric Tuong and Burkhart Wolff. Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection. In Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014.. 2014, 43–52.
[ BibTeX ]

@inproceedings{DBLP:conf/models/LonguetTW14,
	author = "Delphine Longuet and Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff",
	title = "Towards a Tool for Featherweight {OCL:} {A} Case Study On Semantic Reflection",
	booktitle = "Proceedings of the 14th International Workshop on {OCL} and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems {(MODELS} 2014), Valencia, Spain, September 30, 2014.",
	pages = "43--52",
	year = 2014,
	url = "http://ceur-ws.org/Vol-1285/paper05.pdf",
	timestamp = "Wed, 05 Nov 2014 15:39:22 +0100",
	biburl = "http://dblp.uni-trier.de/rec/bib/conf/models/LonguetTW14",
	bibsource = "dblp computer science bibliography, http://dblp.org"
}

Achim D Brucker, Tony Clark, Carolina Dania, Geri Georg, Martin Gogolla, Frédéric Jouault, Ernest Teniente and Burkhart Wolff. Panel Discussion: Proposals for Improving OCL. In Proceedings of the 14th International Workshop on OCL and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems (MODELS 2014), Valencia, Spain, September 30, 2014.. 2014, 83–99.
[ BibTeX ]

@inproceedings{DBLP:conf/models/BruckerCDGGJTW14,
	author = "Achim D. Brucker and Tony Clark and Carolina Dania and Geri Georg and Martin Gogolla and Fr{\'{e}}d{\'{e}}ric Jouault and Ernest Teniente and Burkhart Wolff",
	title = "Panel Discussion: Proposals for Improving {OCL}",
	booktitle = "Proceedings of the 14th International Workshop on {OCL} and Textual Modelling co-located with 17th International Conference on Model Driven Engineering Languages and Systems {(MODELS} 2014), Valencia, Spain, September 30, 2014.",
	pages = "83--99",
	year = 2014,
	url = "http://ceur-ws.org/Vol-1285/paper09.pdf",
	timestamp = "Wed, 05 Nov 2014 15:39:22 +0100",
	biburl = "http://dblp.uni-trier.de/rec/bib/conf/models/BruckerCDGGJTW14",
	bibsource = "dblp computer science bibliography, http://dblp.org"
}

Achim D Brucker, Lukas Brügger and Burkhart Wolff. The Unified Policy Framework (UPF). Archive of Formal Proofs, 2014. \urlhttp://afp.sf.net/entries/UPF.shtml, Formal proof development.
[ BibTeX ]

@article{UPF-AFP,
	author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
	title = "The Unified Policy Framework {(UPF)}",
	journal = "Archive of Formal Proofs",
	month = "",
	year = 2014,
	note = "\url{http://afp.sf.net/entries/UPF.shtml}, Formal proof development",
	issn = "2150-914x"
}

Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Julien Schmaltz. Formal Specification of a Generic Separation Kernel. Archive of Formal Proofs, 2014. \urlhttp://afp.sf.net/entries/CISC-Kernel.shtml, Formal proof development.
[ BibTeX ]

@article{CISC-Kernel-AFP,
	author = "Freek Verbeek and Sergey Tverdyshev and Oto Havle and Holger Blasum and Bruno Langenstein and Werner Stephan and Yakoub Nemouchi and Abderrahmane Feliachi and Burkhart Wolff and Julien Schmaltz",
	title = "Formal Specification of a Generic Separation Kernel",
	journal = "Archive of Formal Proofs",
	month = "",
	year = 2014,
	note = "\url{http://afp.sf.net/entries/CISC-Kernel.shtml}, Formal proof development",
	issn = "2150-914x"
}

Achim D Brucker, Frédéric Tuong and Burkhart Wolff. Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5. Archive of Formal Proofs, 2014. \urlhttp://afp.sf.net/entries/Featherweight_OCL.shtml, Formal proof development.
[ BibTeX | pdf ]

@article{ brucker.ea:featherweight:2014,
	author = "Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff",
	title = "Featherweight OCL: A Proposal for a Machine-Checked Formal Semantics for OCL 2.5",
	journal = "Archive of Formal Proofs",
	month = "",
	year = 2014,
	note = "\url{http://afp.sf.net/entries/Featherweight_OCL.shtml}, Formal proof development",
	issn = "2150-914x",
	abstract = {The Unified Modeling Language (UML) is one of the few modeling languages that is widely used in industry. While UML is mostly known as diagrammatic modeling language (e.g., visualizing class models), it is complemented by a textual language, called Object Constraint Language (OCL). OCL is based on a three-valued logic that turns UML into a formal language. Unfortunately the semantics of this specification language, captured in the "Annex A" of the OCL standard, leads to different interpretations of corner cases. We formalize the core of OCL: denotational definitions, a logical calculus and operational rules that allow for the execution of OCL expressions by a mixture of term rewriting and code compilation. Our formalization reveals several inconsistencies and contradictions in the current version of the OCL standard. Overall, this document is intended to provide the basis for a machine-checked text "Annex A" of the OCL standard targeting at tool implementors.},
	public = "yes",
	classification = "formal",
	categories = "holocl",
	pdf = "http://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-2014.pdf",
	filelabel = "Outline",
	file = "http://www.brucker.ch/bibliography/download/2014/brucker.ea-featherweight-outline-2014.pdf",
	areas = "formal methods, software",
	url = "http://www.brucker.ch/bibliography/abstract/brucker.ea-featherweight-2014"
}

Ana Cavalcanti and M -C Gaudel. Test Selection for Traces Refinement. TCS, Theoretical Computer Science, 2014. available on line, DOI : 10.1016/j.tcs.2014.08.012.
[ BibTeX | pdf ]

@article{RR1568,
	author = "Ana Cavalcanti and M.-C. Gaudel",
	title = "Test Selection for Traces Refinement",
	journal = "TCS, Theoretical Computer Science",
	year = 2014,
	pdf = "https://www.lri.fr/~bibli/Rapports-internes/2013/RR1568.pdf",
	note = "available on line, DOI : 10.1016/j.tcs.2014.08.012"
}

Ana Cavalcanti and Marie-Claude Gaudel. Data Flow coverage for Circus-based testing. In FASE/ETAPS proceedings 8411. 2014, 515-429.
[ BibTeX | pdf ]

@inproceedings{CG14,
	author = "Ana Cavalcanti and Marie-Claude Gaudel",
	title = "Data Flow coverage for {C}ircus-based testing",
	booktitle = "FASE/ETAPS proceedings",
	year = 2014,
	pages = "515-429",
	pdf = "https://www.lri.fr/~bibli/Rapports-internes/2013/RR1567.pdf",
	series = "Lecture Notes in Computer Science",
	volume = 8411,
	x-equipes = "fortesse",
	x-type = "article",
	x-support = "actes"
}

Fatiha Zaidi Huu Nghia Nguyen and Ana Cavalli. A framework for distributed Testing of Timed Composite Systems. In The 21st Asia-Pacific Software Engineering Conference, APSEC 2014. December 2014.
[ BibTeX ]

@inproceedings{ZF_NZC-apsec,
	author = "Huu Nghia Nguyen, Fatiha Zaidi and Ana Cavalli",
	title = "A framework for distributed Testing of Timed Composite Systems",
	booktitle = "The 21st Asia-Pacific Software Engineering Conference, APSEC 2014",
	year = 2014,
	address = "Jeju, Korea",
	month = "december",
	publisher = "IEEE"
}

Delphine Longuet, Frédéric Tuong and Burkhart Wolff. Towards a Tool for Featherweight OCL: A Case Study On Semantic Reflection. In International Workshop on OCL and Textual Modelling 1285. 2014, 43–52.
[ BibTeX | pdf ]

@inproceedings{LTW14,
	author = "Longuet, Delphine and Tuong, Fr{\'e}d{\'e}ric and Wolff, Burkhart",
	title = "Towards a Tool for Featherweight {OCL:} A Case Study On Semantic Reflection",
	booktitle = "International Workshop on {OCL} and Textual Modelling",
	pages = "43--52",
	year = 2014,
	series = "CEUR Workshop Proceedings",
	volume = 1285,
	abstract = "We show how modern proof environments comprising code generators and reflection facilities can be used for the effective construction of a tool for OCL. For this end, we define a UML/OCL meta-model in HOL, a meta-model for Isabelle/HOL in HOL, and a compiling function between them over the vocabulary of the libraries provided by Featherweight OCL. We use the code generator of Isabelle to generate executable code for the compiler, which is bound to a USE tool-like syntax integrated in Isabelle/Featherweight OCL. It generates for an arbitrary class model an object-oriented datatype theory and proves the relevant properties for casts, type-tests, constructors and selectors automatically.",
	pdf = "https://www.lri.fr/~longuet/Publications/LTW14-OCL.pdf"
}

Hernán Ponce de León, Stefan Haar and Delphine Longuet. Distributed Testing of Concurrent Systems: Vector Clocks to the Rescue. In International Conference on Theoretical Aspects of Computing 8687. 2014, 369-387.
[ BibTeX | pdf ]

@inproceedings{PHL14c,
	author = "Ponce de Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine",
	title = "Distributed Testing of Concurrent Systems: Vector Clocks to the Rescue",
	booktitle = "International Conference on Theoretical Aspects of Computing",
	year = 2014,
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 8687,
	pages = "369-387",
	abstract = "The ioco relation has become a standard in model-based conformance testing. The co-ioco conformance relation is an extension of this relation to concurrent systems specified with true-concurrency models. This relation assumes a global control and observation of the system under test, which is not usually realistic in the case of physically distributed systems. Such systems can be partially observed at each of their points of control and observation by the sequences of inputs and outputs exchanged with their environment. Unfortunately, in general, global observation cannot be reconstructed from local ones, so global conformance cannot be decided with local tests. We propose to append time stamps to the observable actions of the system under test in order to regain global conformance from local testing.",
	pdf = "https://www.lri.fr/~longuet/Publications/PdLHL14-ICTAC.pdf"
}

Hernán Ponce de León, Stefan Haar and Delphine Longuet. Model-based Testing for Concurrent Systems with Labelled Event Structures. Software Testing, Verification and Reliability, special issue on Tests and Proofs 24(7):558-590, 2014.
[ BibTeX | pdf ]

@article{PHL14a,
	author = "Ponce de Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine",
	title = "Model-based Testing for Concurrent Systems with Labelled Event Structures",
	journal = "Software Testing, Verification and Reliability, special issue on Tests and Proofs",
	volume = 24,
	number = 7,
	pages = "558-590",
	year = 2014,
	abstract = "We propose a theoretical testing framework and a test generation algorithm for concurrent systems specified with true concurrency models, such as Petri nets or networks of automata. The semantic model of computation of such formalisms are labeled event structures, which allow to represent concurrency explicitly. We introduce the notions of strong and weak concurrency: strongly concurrent events must be concurrent in the implementation, while weakly concurrent ones may eventually be ordered. The ioco type conformance relations for sequential systems rely on the observation of sequences of actions and blockings, thus they are not capable of capturing and exploiting concurrency of non sequential behaviors. We propose an extension of ioco for labeled event structures, named co-ioco, allowing to deal with strong and weak concurrency. We extend the notions of test cases and test execution to labeled event structures, and give a test generation algorithm building a complete test suite for co-ioco.",
	pdf = "http://www.lri.fr/~longuet/Publications/PdLHL14-STVR.pdf"
}

Hernán Ponce de León, Stefan Haar and Delphine Longuet. Model-based Testing for Concurrent Systems: Unfolding-based Test Selection. Software Tools for Technology Transfer, selected papers of ICTAC'14, 2014. To appear.
[ BibTeX | pdf ]

@article{PHL14b,
	author = "Ponce de Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine",
	title = "Model-based Testing for Concurrent Systems: Unfolding-based Test Selection",
	journal = "Software Tools for Technology Transfer, selected papers of ICTAC'14",
	year = 2014,
	abstract = "Model-based testing has mainly focused on models where concurrency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order to test such concurrent systems, we choose to use Petri nets as specifications and define a concurrent conformance relation named co-ioco. We present a test generation algorithm based on Petri net unfolding able to build a complete test suite w.r.t our co-ioco conformance relation. In addition we propose several coverage criteria that allow to select finite prefixes of an unfolding in order to build manageable test suites.",
	pdf = "http://www.lri.fr/~longuet/Publications/PdLHL14-STTT.pdf",
	note = "To appear"
}

Thierry Jéron, Margus Veanes and Burkhart Wolff. Symbolic Methods in Testing (Dagstuhl Seminar 13021). Dagstuhl Reports 3(1):1–29, 2013.
[ BibTeX ]

@article{jron_et_al:DR:2013:4006,
	author = "Thierry J{\'e}ron and Margus Veanes and Burkhart Wolff",
	title = "{Symbolic Methods in Testing (Dagstuhl Seminar 13021)}",
	pages = "1--29",
	journal = "Dagstuhl Reports",
	issn = "2192-5283",
	year = 2013,
	volume = 3,
	number = 1,
	editor = "Thierry J{\'e}ron and Margus Veanes and Burkhart Wolff",
	publisher = "Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik",
	address = "Dagstuhl, Germany",
	url = "http://drops.dagstuhl.de/opus/volltexte/2013/4006",
	urn = "urn:nbn:de:0030-drops-40060",
	doi = "10.4230/DagRep.3.1.1",
	area = "logical_representations",
	annote = "Keywords: Automated Deduction, White-box testing, Black-box Testing, Fuzz-Testing, Unit-Testing, Theorem prover-based Testing"
}

Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel and Burkhart Wolff. The Circus Testing Theory Revisited in Isabelle/HOL. In Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods(ICFEM). Series Lecture Notes in Computer Science, number 8144, Springer-Verlag, 2013.
[ BibTeX | pdf ]

@incollection{feliachi.ea:cirta:2013,
	abstract = "Formal specifications provide strong bases for testing and bring powerful techniques and technologies. Expressive formal specification languages combine large data domain and behavior. Thus, symbolic methods have raised particular interest for test generation techniques. Integrating formal testing in proof environments such as Isabelle/HOL is referred to as “theorem-prover based testing”. Theorem-prover based testing can be adapted to a specific specification language via a representation of its formal semantics, paving the way for specific support of its constructs. The main challenge of this approach is to reduce the gap between pen-and-paper semantics and formal mechanized theories. In this paper we consider testing based on the Circus specification language. This language integrates the notions of states and of complex data in a Z-like fashion with communicating processes inspired from CSP. We present a machine-checked formalization in Isabelle/HOL of this lan- guage and its testing theory. Based on this formal representation of the semantics we revisit the original associated testing theory. We discovered unforeseen simplifications in both definitions and symbolic computations. The approach lends itself to the construction of a tool, that directly uses semantic definitions of the language as well as derived rules of its testing theory, and thus provides some powerful sym- bolic computation machinery to seamlessly implement them both in a technical environment.",
	keywords = "symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing",
	location = "Wellington",
	author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Makarius Wenzel and Burkhart Wolff",
	booktitle = "Formal Methods and Software Engineering - 15th International Conference on Formal Engineering Methods(ICFEM)",
	language = "USenglish",
	publisher = "Springer-Verlag",
	address = "Heidelberg",
	series = "Lecture Notes in Computer Science",
	number = 8144,
	title = "The Circus Testing Theory Revisited in Isabelle/HOL",
	categories = "holtestgen",
	classification = "conference",
	areas = "formal testing, semantics, formal methods",
	year = 2013,
	pdf = "http://www.lri.fr/~wolff/papers/conf/2013-Circus-testing.pdf"
}

Achim D Brucker, Lukas Brügger and Burkhart Wolff. HOL-TestGen/FW: An Environment for Specification-based Firewall Conformance Testing. In International Colloquium on Theoretical Aspects of Computing (ICTAC). Series Lecture Notes in Computer Science, number 8049, Springer-Verlag, 2013.
[ BibTeX | pdf ]

@incollection{ brucker.ea:hol-testgen-fw:2013,
	abstract = "The HOL-TestGen environment is conceived as a system for modeling and semi-automated test generation with an emphasis on expressive power and generality. However, its underlying technical framework Isabelle/HOL supports the customization as well as the development of highly automated add-ons working in specific application domains. In this paper, we present HOL-TestGen/fw, an add-on for the test framework HOL-TestGen, that allows for testing the conformance of firewall implementations to high-level security policies. Based on generic theories specifying a security-policy language, we developed specific theories for network data and firewall policies. On top of these firewall specific theories, we provide mechanisms for policy transformations based on derived rules and adapted code-generators producing test drivers. Our empirical evaluations shows that HOL-TestGen/fw is a competitive environment for testing firewalls or high-level policies of local networks.",
	keywords = "symbolic test case generations, black box testing, theorem proving, network security, firewall testing, conformance testing",
	location = "Shanghai",
	author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
	booktitle = "International Colloquium on Theoretical Aspects of Computing (ICTAC)",
	language = "USenglish",
	publisher = "Springer-Verlag",
	address = "Heidelberg",
	series = "Lecture Notes in Computer Science",
	number = 8049,
	title = "HOL-TestGen/FW: An Environment for Specification-based Firewall Conformance Testing",
	categories = "holtestgen",
	classification = "conference",
	areas = "security, formal methods",
	year = 2013,
	pdf = "http://www.lri.fr/~wolff/papers/conf/2013-ictac-hol-testgen-fw.pdf"
}

Bruno Barras, Lourdes Del Carmen González-Huesca, Hugo Herbelin, Yann Régis-Gianas, Enrico Tassi, Makarius Wenzel and Burkhart Wolff. Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems. In MKM/Calculemus/DML 7961. 2013, 359-363.
[ BibTeX | pdf ]

@inproceedings{DBLP:conf/mkm/BarrasGHRTWW13,
	author = "Bruno Barras and Lourdes Del Carmen Gonz{\'a}lez-Huesca and Hugo Herbelin and Yann R{\'e}gis-Gianas and Enrico Tassi and Makarius Wenzel and Burkhart Wolff",
	title = "Pervasive Parallelism in Highly-Trustable Interactive Theorem Proving Systems",
	booktitle = "MKM/Calculemus/DML",
	year = 2013,
	pages = "359-363",
	doi = "10.1007/978-3-642-39320-4_29",
	pdf = "http://www.lri.fr/~wolff/papers/conf/CICM13-PervasiveParallsm.pdf",
	area = "logical_representations",
	bibsource = "DBLP, http://dblp.uni-trier.de",
	classification = "conference",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 7961,
	abstract = "Interactive theorem proving is a technology of fundamental importance for mathematics and computer-science. It is based on expressive logical foundations and implemented in a highly trustable way. Applications include huge mathematical proofs and semi-automated verifications of complex software systems. Interactive development of larger and larger proofs increases the demand for computing power, which means explicit parallelism on current multicore hardware. The architecture of contemporary interactive provers such as Coq, Isabelle or the HOL family goes back to the influential LCF system from 1979, which has pioneered key principles like correctness by construction for primitive inferences and definitions, free programmability in userspace via ML, and toplevel command interaction. Both Coq and Isabelle have elaborated the prover architecture over the years, driven by the demands of sophisticated proof procedures, derived specification principles, large libraries of formalized mathematics etc. Despite this success, the operational model of interactive proof checking was limited by sequential ML evaluation and the sequential read-eval-print loop, as inherited from LCF."
}

Achim D Brucker, Abderrahmane Feliachi, Yakoub Nemouchi and Burkhart Wolff. Test Program Generation for a Microprocessor – A Case-Study. In Proceedings of the 6th Intl. Conf. on Test and Proof (TAP '13) LNCS 7942. 2013, 76–95.
[ BibTeX | pdf ]

@inproceedings{Brucker:2013:TAP,
	author = "Brucker, Achim D. and Feliachi, Abderrahmane and Nemouchi, Yakoub and Wolff, Burkhart",
	title = "Test Program Generation for a Microprocessor -- A Case-Study",
	booktitle = "Proceedings of the 6th Intl. Conf. on Test and Proof (TAP '13)",
	series = "Lecture Notes in Computer Science",
	volume = "LNCS 7942",
	year = 2013,
	location = "Budapest, Hungaria",
	pages = "76--95",
	numpages = 20,
	classification = "conference",
	pdf = "http://www.lri.fr/~wolff/papers/conf/2013-TapPresentation.pdf",
	publisher = "Springer LNCS",
	doi = "10.1007/978-3-642-38916-0_5",
	area = "logical_representations",
	domain = "os_test",
	abstract = "Certifications of critical security or safety system properties are becoming increasingly important for a wide range of products. Certifying large systems like operating systems up to Common Criteria EAL 4 is common practice today, and higher certification levels are at the brink of becoming reality. To reach EAL 7 one has to formally verify properties on the specification as well as test the implementation thoroughly. This includes tests of the used hardware platform underlying a proof architecture to be certified. In this paper, we address the latter problem: we present a case study that uses a formal model of a microprocessor and generate test programs from it. These test programs validate that a microprocessor implements the specified instruction set correctly. We built our case study on an existing model that was, together with an operating system, developed in Isabelle/HOL. We use HOL-TestGen, a model-based testing environment which is an extension of Isabelle/HOL. We develop several conformance test scenarios, where processor models were used to synthesize test programs that were run against real hard- ware in the loop. Our test case generation approach directly benefits from the existing models and formal proofs in Isabelle/HOL.",
	keywords = "test program generation, symbolic test case generations, black box testing, white box testing, theorem proving, interactive testing"
}

Burkhart Wolff, Marie-Claude Gaudel and Abderrahmane Feliachi (eds.). Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers LNCS 7681. Springer, 2013.
[ BibTeX ]

@proceedings{DBLP:conf/utp/2008,
	editor = "Burkhart Wolff and Marie-Claude Gaudel and Abderrahmane Feliachi",
	title = "Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers",
	booktitle = "UTP",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = "LNCS 7681",
	year = 2013,
	isbn = "978-3-642-35704-6",
	activity = "something"
}

Achim D Brucker, Delphine Longuet, Frédéric Tuong and Burkhart Wolff. On the Semantics of Object-Oriented Data Structures and Path Expressions. In OCL@MoDELS 1092. 2013, 23-32.
[ BibTeX ]

@inproceedings{DBLP:conf/models/BruckerLTW13,
	author = "Achim D. Brucker and Delphine Longuet and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff",
	title = "On the {S}emantics of {O}bject-{O}riented {D}ata {S}tructures and {P}ath {E}xpressions",
	booktitle = "OCL@MoDELS",
	year = 2013,
	pages = "23-32",
	ee = "http://ceur-ws.org/Vol-1092/brucker.pdf",
	publisher = "CEUR-WS.org",
	series = "CEUR Workshop Proceedings",
	volume = 1092
}

Achim D Brucker, Dan Chiorean, Tony Clark, Birgit Demuth, Martin Gogolla, Dimitri Plotnikov, Bernhard Rumpe, Edward D Willink and Burkhart Wolff. Report on the Aachen OCL Meeting. In OCL@MoDELS 1092. 2013, 103-111.
[ BibTeX ]

@inproceedings{DBLP:conf/models/BruckerCCDGPRWW13,
	author = "Achim D. Brucker and Dan Chiorean and Tony Clark and Birgit Demuth and Martin Gogolla and Dimitri Plotnikov and Bernhard Rumpe and Edward D. Willink and Burkhart Wolff",
	title = "Report on the Aachen OCL Meeting",
	booktitle = "OCL@MoDELS",
	year = 2013,
	pages = "103-111",
	ee = "http://ceur-ws.org/Vol-1092/aachen.pdf",
	publisher = "CEUR-WS.org",
	series = "CEUR Workshop Proceedings",
	volume = 1092
}

Achim D Brucker and Burkhart Wolff. On Theorem Prover-based Testing. Formal Asp. Comput. (FAOC) 25(5):683–721, 2013.
[ BibTeX | pdf ]

@article{brucker.ea:2012,
	author = "Achim D. Brucker and Burkhart Wolff",
	title = "On {T}heorem {P}rover-based {T}esting",
	journal = "Formal Asp. Comput. (FAOC)",
	year = 2013,
	month = "",
	volume = 25,
	number = 5,
	pages = "683--721",
	abstract = "\emph{HOL-TestGen} is a specification and test case generation environment extending the interactive theorem prover Isabelle/HOL. As such, HOL-TestGen allows for an integrated workflow supporting interactive theorem proving, test case generation, and test data generation. The HOL-TestGen method is two-staged: first, the original formula 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. Due to the generality of the underlying framework, our system can be used for black-box unit, sequence, reactive sequence and white-box test scenarios. Although based on particularly clean theoretical foundations, the system can be applied for substantial case-studies.",
	pdf = "http://www.lri.fr/~wolff/papers/journals/brucker.ea-hol-testgen-2008.rev-1.pdf",
	keywords = "Isabelle/HOL, Theorem proving, Model-based Testing, Program-based Testing, Testcase Generation",
	doi = "10.1007/s00165-012-0222-y",
	area = "logical_representations",
	classification = "journal"
}

Achim D Brucker, Delphine Longuet, Frédéric Tuong and Burkhart Wolff. On the Semantics of Object-oriented Data Structures and Path Expressions (Extended Version). Number 1565, Laboratoire en Recherche en Informatique (LRI), Université Paris-Sud 11, France, 2013.
[ BibTeX | pdf ]

@techreport{ brucker.ea:path-expressions:2013-b,
	author = "Achim D. Brucker and Delphine Longuet and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff",
	title = "On the Semantics of Object-oriented Data Structures and Path Expressions (Extended Version)",
	booktitle = "Workshop on OCL and Textual Modelling (OCL 2013)",
	year = 2013,
	abstract = "\UML/\OCL is perceived as the de-facto standard for specifying object-oriented models in general and data models in particular. Since recently, all data types of \UML/\OCL comprise two different exception elements: \inlineocl{invalid} (``bottom'' in semantics terminology) and \inlineocl{null} (for ``non-existing element''). This has far-reaching consequences on both the logical and algebraic properties of \OCL expressions as well as the path expressions over object-oriented data structures, \ie, class models. In this paper, we present a formal semantics for object-oriented data models in which all data types and, thus, all class attributes and path expressions, support \inlineocl{invalid} and \inlineocl{null}. Based on this formal semantics, we present a set of \OCL test cases that can be used for evaluating the support of \inlineocl{null} and \inlineocl{invalid} in \OCL tools.",
	classification = "unrefereed",
	categories = "holocl",
	url = "http://www.brucker.ch/bibliography/abstract/brucker.ea-path-expressions-2013-b",
	number = 1565,
	institution = "Laboratoire en Recherche en Informatique (LRI), Universit\'e Paris-Sud 11, France",
	areas = "formal methods, software",
	keywords = "Object-oriented Data Structures, Path Expressions, Featherweight OCL, Null, Invalid, Formal Semantics",
	public = "yes",
	pdf = "http://www.brucker.ch/bibliography/download/2013/brucker.ea-path-expressions-2013-b.pdf"
}

Ana Cavalcanti and M -C Gaudel. A note on Test Selection for conf Refinement. Rapport LRI 1569, Université de Paris-Sud, 2013.
[ BibTeX | pdf ]

@techreport{RR1569,
	author = "Ana Cavalcanti and M.-C. Gaudel",
	title = "A note on Test Selection for conf Refinement",
	institution = "Universit\'e de Paris-Sud",
	year = 2013,
	type = "Rapport {LRI}",
	number = 1569,
	pdf = "https://www.lri.fr/~bibli/Rapports-internes/2013/RR1569.pdf"
}

Abderrahmane Feliachi, Marie-Claude Gaudel, Makarius Wenzel and Burkhart Wolff. The Circus Testing Theory Revisited in Isabelle/HOL. In 15th International Conference on Formal Engineering Methods, ICFEM 2013 8144. 2013, 131-147.
[ BibTeX | pdf ]

@inproceedings{DBLP:conf/icfem/FeliachiGWW13,
	author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Makarius Wenzel and Burkhart Wolff",
	title = "The {C}ircus Testing Theory Revisited in {Isabelle/HOL}",
	booktitle = "15th International Conference on Formal Engineering Methods, ICFEM 2013",
	year = 2013,
	pages = "131-147",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 8144,
	pdf = "http://www.lri.fr/~mcg/PDF/ICFEM2013.pdf"
}

Burkhart Wolff, Marie-Claude Gaudel and Abderrahmane Feliachi (eds.). Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers 7681. Springer, 2013.
[ BibTeX ]

@proceedings{DBLP:conf/utp/2012,
	editor = "Burkhart Wolff and Marie-Claude Gaudel and Abderrahmane Feliachi",
	title = "Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers",
	booktitle = "UTP",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 7681,
	year = 2013,
	isbn = "978-3-642-35704-6, 978-3-642-35705-3",
	ee = "http://dx.doi.org/10.1007/978-3-642-35705-3",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

Marie-Claude Gaudel, Richard Lassaigne, Frédéric Magniez and Michel Rougemont. Some approximations in Model Checking and Testing. CoRR abs/1304.5199, 2013.
[ BibTeX ]

@article{DBLP:journals/corr/abs-1304-5199,
	author = "Marie-Claude Gaudel and Richard Lassaigne and Fr{\'e}d{\'e}ric Magniez and Michel de Rougemont",
	title = "Some approximations in Model Checking and Testing",
	journal = "CoRR",
	volume = "abs/1304.5199",
	year = 2013,
	ee = "http://arxiv.org/abs/1304.5199",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

Johan Oudinet, Alain Denise and Marie-Claude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. TCS, Theoretical Computer Science 502:165-176, 2013. extended version of \citegascom10.
[ BibTeX | pdf ]

@article{TCS:2012,
	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",
	journal = "TCS, Theoretical Computer Science",
	year = 2013,
	volume = 502,
	pages = "165-176",
	publisher = "Elsevier",
	note = "extended version of \cite{gascom10}",
	pdf = "http://www.lri.fr/~mcg/PDF/TCSfinal.pdf"
}

Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaïdi. Invariants for finite instances and beyond. In Formal Methods in Computer-Aided DEsign, FMCAD. October 2013, 61-68.
[ BibTeX ]

@inproceedings{ZF_CGKMZ13,
	author = {Sylvain Conchon and Amit Goel and Sava Krstic and Alain Mebsout and Fatiha Za\"{i}di},
	title = "Invariants for finite instances and beyond",
	booktitle = "Formal Methods in Computer-Aided DEsign, FMCAD",
	pages = "61-68",
	year = 2013,
	address = "Portland, USA",
	month = "october",
	publisher = "IEEE"
}

Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. Automatic skeleton generation for data-aware service choreographies. In IEEE 24th International Symposium on Software Reliability Engineerinf, ISSRE 2013. November 2013, 320-329.
[ BibTeX ]

@inproceedings{ZF_NPZ13-issre,
	author = "Huu Nghia Nguyen and Pascal Poizat and Fatiha Zaidi",
	title = "Automatic skeleton generation for data-aware service choreographies",
	booktitle = "IEEE 24th International Symposium on Software Reliability Engineerinf, ISSRE 2013",
	pages = "320-329",
	year = 2013,
	address = "Pasadena, USA",
	month = "november",
	publisher = "IEEE"
}

Achim D Brucker, Delphine Longuet, Frédéric Tuong and Burkhart Wolff. On the Semantics of Object-oriented Data Structures and Path Expressions. In International Workshop on OCL and Textual Modelling 1092. 2013, 23-32.
[ BibTeX | pdf ]

@inproceedings{BLTW-OCL13,
	author = "Brucker, Achim D. and Longuet, Delphine and Tuong, Fr{\'e}d{\'e}ric and Wolff, Burkhart",
	title = "On the Semantics of Object-oriented Data Structures and Path Expressions",
	booktitle = "International Workshop on {OCL} and Textual Modelling",
	year = 2013,
	pages = "23-32",
	series = "CEUR Workshop Proceedings",
	volume = 1092,
	abstract = {UML/OCL is perceived as the de-facto standard for specifying object-oriented models in general and data models in particular. Since recently, all data types of UML/OCL comprise two different exception elements: invalid ("bottom" in semantics terminology) and null (for "non-existing element"). This has far-reaching consequences on both the logical and algebraic properties of OCL expressions as well as the path expressions over object-oriented data structures, i. e., class models. In this paper, we present a formal semantics for object-oriented data models in which all data types and, thus, all class attributes and path expressions, support invalid and null. Based on this formal semantics, we present a set of OCL test cases that can be used for evaluating the support of null and invalid in OCL tools.},
	pdf = "https://www.lri.fr/~longuet/Publications/BLTW13-OCL.pdf"
}

Hernán Ponce de León, Stefan Haar and Delphine Longuet. Unfolding-based Test Selection for Concurrent Conformance. In International Conference and Testing Software and Systems 8254. 2013, 98-113.
[ BibTeX | pdf ]

@inproceedings{PHL13,
	author = "Ponce de Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine",
	title = "Unfolding-based Test Selection for Concurrent Conformance",
	booktitle = "International Conference and Testing Software and Systems",
	year = 2013,
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 8254,
	pages = "98-113",
	abstract = "Model-based testing has mainly focused on models where currency is interpreted as interleaving (like the ioco theory for labeled transition systems), which may be too coarse when one wants concurrency to be preserved in the implementation. In order to test such concurrent systems, we choose to use Petri nets as specifications and define a concurrent conformance relation named co-ioco. We propose a test generation algorithm based on Petri net unfolding able to build a complete test suite w.r.t our co-ioco conformance relation. In addition we propose a coverage criterion based on a dedicated notion of complete prefixes that selects a manageable test suite.",
	pdf = "http://www.lri.fr/~longuet/Publications/PdLHL13-ICTSS.pdf"
}

Romain Aissat and Jean-Yves Pierron. Méthode de validation par génération alétoire de chemins dans des modèles à base d'automates communicants. In Approches Formelles dans l'Assistance au Développement de Logiciels. 2013, 33 – 47.
[ BibTeX ]

@inproceedings{ap13,
	author = "Aissat, Romain and Pierron, Jean-Yves",
	title = "M\'ethode de validation par g\'en\'eration al\'etoire de chemins dans des mod\`eles \`a base d'automates communicants",
	booktitle = "Approches Formelles dans l'Assistance au D\'eveloppement de Logiciels",
	year = 2013,
	month = "avril",
	pages = "33 -- 47"
}

Achim D Brucker and Burkhart Wolff. Featherweight OCL: a study for the consistent semantics of OCL 2.3 in HOL. In Proceedings of the 12th Workshop on OCL and Textual Modelling. 2012, 19–24.
[ BibTeX | pdf ]

@inproceedings{Brucker:2012:FOS:2428516.2428520,
	author = "Brucker, Achim D. and Wolff, Burkhart",
	title = "Featherweight OCL: a study for the consistent semantics of OCL 2.3 in HOL",
	booktitle = "Proceedings of the 12th Workshop on OCL and Textual Modelling",
	series = "OCL '12",
	year = 2012,
	isbn = "978-1-4503-1799-3",
	location = "Innsbruck, Austria",
	pages = "19--24",
	numpages = 6,
	url = "10.1145/2428516.2428520",
	doi = "10.1145/2428516.2428520",
	acmid = 2428520,
	pdf = "http://www.lri.fr/~wolff/papers/workshop/featherweight-ocl.pdf",
	publisher = "ACM",
	address = "New York, NY, USA",
	area = "logical_representations",
	domain = "os_test",
	classification = "conference",
	keywords = "HOL-OCL, OCL, formal semantics"
}

Abderrahmane Feliachi, Burkhart Wolff and Marie-Claude Gaudel. Isabelle/Circus. Archive of Formal Proofs, 2012. \urlhttp://afp.sourceforge.net/entries/Circus.shtml, Formal proof development.
[ BibTeX ]

@article{Feliachi-Wolff-Gaudel-AFP12,
	author = "Abderrahmane Feliachi and Burkhart Wolff and Marie-Claude Gaudel",
	title = "Isabelle/Circus",
	journal = "Archive of Formal Proofs",
	month = "",
	year = 2012,
	note = "\url{http://afp.sourceforge.net/entries/Circus.shtml}, Formal proof development",
	area = "logical_representations",
	abstract = "The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's Unifying Theories of Programming (UTP). Isabelle/Circus is a formalization of the UTP and the Circus language in Isabelle/HOL. It contains proof rules and tactic support that allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). The Isabelle/Circus environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus. This article contains an extended version of corresponding VSTTE Paper together with the complete formal development of its underlying commented theories.",
	issn = "2150-914x"
}

Achim D Brucker, Lukas Brügger, Matthias P Krieger and Burkhart Wolff. HOL-TestGen 1.7.0 User Guide. Number 1551, Laboratoire en Recherche en Infromatique (LRI), Université Paris-Sud 11, France, 2012.
[ BibTeX | pdf ]

@techreport{ brucker.ea:hol-testgen:2012,
	author = {Achim D. Brucker and Lukas Br{\"u}gger and Matthias P. Krieger and Burkhart Wolff},
	institution = "Laboratoire en Recherche en Infromatique (LRI), Universit\'e Paris-Sud 11, France",
	language = "USenglish",
	month = "",
	title = "{HOL-TestGen} 1.7.0 User Guide",
	categories = "testing,holtestgen",
	classification = "unrefereed",
	areas = "formal methods, software",
	keywords = "symbolic test case generations, black box testing, theorem proving, Isabelle/HOL",
	year = 2012,
	number = 1551,
	area = "logical_representations",
	num_pages = 120,
	pdf = "http://www.brucker.ch/bibliography/download/2012/brucker.ea-hol-testgen-2012.pdf",
	public = "yes",
	url = "http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2012"
}

Abderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff. Isabelle/Circus: A Process Specification and Verification Environment. In VSTTE LNCS 7152. 2012, 243-260.
[ BibTeX | pdf ]

@inproceedings{feliachigw12,
	author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
	title = "Isabelle/{C}ircus: A Process Specification and Verification Environment",
	booktitle = "VSTTE",
	year = 2012,
	pages = "243-260",
	series = "Lecture Notes in Computer Science",
	volume = "LNCS 7152",
	isbn = "978-3-642-27704-7",
	ee = "http://dx.doi.org/10.1007/978-3-642-27705-4_20",
	doi = "10.1007/978-3-642-27705-4_20",
	abstract = {The Circus specification language combines elements for complex data and behavior specifications, using an integration of Z and CSP with a refinement calculus. Its semantics is based on Hoare and He's unifying theories of programming (UTP). We develop a machine-checked, formal semantics based on a "shallow embedding" of Circus in Isabelle/UTP (our semantic theory of UTP based on Isabelle/HOL). We derive proof rules from this semantics and imple- ment tactic support that finally allows for proofs of refinement for Circus processes (involving both data and behavioral aspects). This proof environment supports a syntax for the semantic definitions which is close to textbook presentations of Circus.},
	pdf = "http://www.lri.fr/~wolff/papers/conf/VSTTE-IsabelleCircus11.pdf",
	classification = "conference",
	area = "logical_representations",
	bibsource = "DBLP, http://dblp.uni-trier.de",
	crossref = "DBLP:conf/vstte/2012",
	x-equipes = "fortesse",
	x-type = "article",
	x-support = "actes"
}

Abderrahmane Feliachi. Semantics-Based Testing for Circus. Phd Thesis, Université Paris Sud, December 2012. Directeurs: Prof. Marie-Claude Gaudel and Prof. Burkhart Wolff.
[ BibTeX ]

@phdthesis{feliachi2012,
	author = "Abderrahmane Feliachi",
	title = "Semantics-Based Testing for Circus",
	school = "Universit\'e Paris Sud",
	year = 2012,
	month = "December",
	note = "Directeurs: Prof. Marie-Claude Gaudel and Prof. Burkhart Wolff",
	x-equipes = "fortesse"
}

Marie-Claude Gaudel. Le test de logiciel : pourquoi et comment. Rayonnement du CNRS, pages 33-39, March 2012.
[ BibTeX | pdf ]

@article{CNRS:2012,
	author = "Marie-Claude Gaudel",
	title = "Le test de logiciel : pourquoi et comment",
	journal = "Rayonnement du CNRS",
	year = 2012,
	month = "March",
	pages = "33-39",
	publisher = "CNRS",
	pdf = "http://www.lri.fr/~mcg/PDF/RayCNRS.pdf"
}

Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet and Sylvain Peyronnet. Coverage-Biased Random Exploration of Large Models and Application to Testing. STTT, International Journal on Software Tools for Technology Transfer 14(1):73-93, 2012.
[ BibTeX | pdf ]

@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 = 2012,
	volume = 14,
	number = 1,
	pages = "73-93",
	publisher = "Springer",
	pdf = "http://www.lri.fr/~mcg/PDF/STTTfinal.pdf"
}

Sylvain Conchon, Amit Goel, Sava Krstic, Alain Mebsout and Fatiha Zaïdi. Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems. In 24th International Conference, CAV 2012 7358. July 2012, 718–724.
[ BibTeX ]

@inproceedings{ZF_CGKMZ,
	author = {Sylvain Conchon and Amit Goel and Sava Krstic and Alain Mebsout and Fatiha Za\"{i}di},
	title = "Cubicle: A Parallel SMT-Based Model Checker for Parameterized Systems",
	booktitle = "24th International Conference, CAV 2012",
	pages = "718--724",
	year = 2012,
	volume = 7358,
	series = "LNCS",
	address = "Berkeley",
	month = "July",
	publisher = "Springer"
}

Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. Online Verification of Value-Passing Choreographies through Property-Oriented Passive Testing. In IEEE (ed.). 14th IEEE International High Assurance Systems Engineering Symposium (HASE 12). November 2012, 106-113.
[ BibTeX ]

@inproceedings{ZF_NPZ12-hase,
	author = "Huu Nghia Nguyen and Pascal Poizat and Fatiha Zaidi",
	title = "Online Verification of Value-Passing Choreographies through Property-Oriented Passive Testing",
	booktitle = "14th IEEE International High Assurance Systems Engineering Symposium (HASE 12)",
	pages = "106-113",
	year = 2012,
	editor = "IEEE",
	month = "November"
}

Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies. In International Conference on Service Oriented Computing (ICSOC 12). 2012, 525–532.
[ BibTeX ]

@inproceedings{ZF_NPZ12-icsoc,
	author = "Huu Nghia Nguyen and Pascal Poizat and Fatiha Zaidi",
	title = "A Symbolic Framework for the Conformance Checking of Value-Passing Choreographies",
	booktitle = "International Conference on Service Oriented Computing (ICSOC 12)",
	pages = "525--532",
	year = 2012,
	month = "Novembe"
}

Huu Nghia Nguyen, Pascal Poizat and Fatiha Zaidi. Passive Conformance Testing of Service Choreographies. In ACM (ed.). 27th ACM Symposium on Applied Computing (SAC 2012). March 2012, 1528-1535.
[ BibTeX ]

@inproceedings{ZF_NPZ12,
	author = "Huu Nghia Nguyen and Pascal Poizat and Fatiha Zaidi",
	title = "Passive Conformance Testing of Service Choreographies",
	booktitle = "27th ACM Symposium on Applied Computing (SAC 2012)",
	year = 2012,
	pages = "1528-1535",
	editor = "ACM",
	month = "March"
}

Johan Jeuring, John A Campbell, Jacques Carette, Gabriel Dos Reis, Petr Sojka, Makarius Wenzel and Volker Sorge (eds.). Intelligent Computer Mathematics –- 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings 7362. Springer, 2012.
[ BibTeX ]

@proceedings{CICM-2012,
	editor = "Johan Jeuring and John A. Campbell and Jacques Carette and Dos Reis, Gabriel and Petr Sojka and Makarius Wenzel and Volker Sorge",
	title = "Intelligent Computer Mathematics --- 11th International Conference, AISC 2012, 19th Symposium, Calculemus 2012, 5th International Workshop, DML 2012, 11th International Conference, MKM 2012, Systems and Projects, Held as Part of CICM 2012, Bremen, Germany, July 8-13, 2012. Proceedings",
	booktitle = "AISC/MKM/Calculemus",
	publisher = "Springer",
	series = "LNCS",
	volume = 7362,
	year = 2012
}

Makarius Wenzel. Isabelle/jEdit –- A Prover IDE within the PIDE Framework. In Johan Jeuring al (ed.). Intelligent Computer Mathematics –- 11th International Conference (CICM/MKM 2012) 7362. 2012.
[ BibTeX ]

@inproceedings{Wenzel:2012:PIDE,
	author = "Makarius Wenzel",
	title = "{Isabelle/jEdit} --- A {Prover IDE} within the {PIDE} Framework",
	booktitle = "Intelligent Computer Mathematics --- 11th International Conference (CICM/MKM 2012)",
	year = 2012,
	editor = "Johan Jeuring et al",
	volume = 7362,
	series = "LNCS",
	publisher = "Springer"
}

Delphine Longuet. Global and Local Testing from Message Sequence Charts. In Symposium on Applied Computing. 2012, 1332-1338.
[ BibTeX | pdf ]

@inproceedings{Lon12,
	author = "Longuet, Delphine",
	title = "Global and Local Testing from Message Sequence Charts",
	booktitle = "Symposium on Applied Computing",
	pages = "1332-1338",
	publisher = "ACM",
	year = 2012,
	abstract = "Message Sequence Charts are a widely used formalism for describing scenarios a communicating system must be able to perform. We study in this paper different formal frameworks for testing from MSCs. We first consider a setting where all the processes of the system can be controlled and observed globally. Then we study a setting where the system is tested from the point of view of each process individually, observations remaining local or being gathered at the end of each test. In each setting, we define a conformance relation based on global or local observations, for which we build an exhaustive test set. Moreover, we gather the conditions making local testing as powerful as global testing.",
	pdf = "http://www.lri.fr/~longuet/Publications/Lon12-SAC.pdf"
}

Hernán Ponce de León, Stefan Haar and Delphine Longuet. Conformance Relations for Labeled Event Structures. In Tests and Proofs 7305. 2012, 83-98.
[ BibTeX | pdf ]

@inproceedings{PHL12,
	author = "Ponce de Le{\'o}n, Hern{\'a}n and Haar, Stefan and Longuet, Delphine",
	title = "Conformance Relations for Labeled Event Structures",
	booktitle = "Tests and Proofs",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 7305,
	year = 2012,
	pages = "83-98",
	abstract = "We propose a theoretical framework for testing concurrent systems from true concurrency models like Petri nets or networks of automata. The underlying model of computation of such formalisms are labeled event structures, which allow to represent concurrency explicitly. The activity of testing relies on the definition of a conformance relation that depends on the observable behaviors on the system under test, which is given for sequential systems by ioco type relations. However, these relations are not capable of capturing and exploiting concurrency of non sequential behavior. We study different conformance relations for labeled event structures, relying on different notions of observation, and investigate their properties and connections.",
	pdf = "http://www.lri.fr/~longuet/Publications/PdLHL12-TAP.pdf"
}

Abderrahmane Feliachi. Representing Circus Operational Semantics in Isabelle/HOL. Number 1544, LRI, http://www.lri.fr/Rapports-internes, August 2011.
[ BibTeX | pdf ]

@techreport{feliachi11rapport-lri,
	author = "Abderrahmane Feliachi",
	title = "Representing {C}ircus {O}perational {S}emantics in {I}sabelle/{HOL}",
	institution = "LRI, http://www.lri.fr/Rapports-internes",
	year = 2011,
	number = 1544,
	address = "Universit{\'e} Paris-Sud XI",
	month = "August",
	pdf = "http://www.lri.fr/~bibli/Rapports-internes/2011/RR1544.pdf",
	x-equipes = "fortesse",
	x-type = "article",
	x-support = "rapport"
}

Jordi Cabot, Robert Clarisó, Martin Gogolla and Burkhart Wolff. Preface (OCL 2011 Proceedings). ECEASST 44, 2011.
[ BibTeX ]

@article{DBLP:journals/eceasst/CabotCGW11,
	author = "Jordi Cabot and Robert Claris{\'o} and Martin Gogolla and Burkhart Wolff",
	title = "Preface (OCL 2011 Proceedings)",
	journal = "ECEASST",
	volume = 44,
	year = 2011,
	ee = "http://journal.ub.tu-berlin.de/eceasst/article/view/666",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

Burkhart Wolff and Fatiha Za\"\idi (eds.). Testing Software and Systems - 23rd IFIP WG 6.1 International Conference, ICTSS 2011, Paris, France, November 7-10, 2011. Proceedings 7019. Springer, 2011.
[ BibTeX ]

@proceedings{DBLP:conf/pts/2011,
	editor = {Burkhart Wolff and Fatiha Za\"{\i}di},
	title = "Testing Software and Systems - 23rd IFIP WG 6.1 International Conference, ICTSS 2011, Paris, France, November 7-10, 2011. Proceedings",
	booktitle = "ICTSS",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 7019,
	year = 2011,
	isbn = "978-3-642-24579-4",
	ee = "http://dx.doi.org/10.1007/978-3-642-24580-0",
	doi = "10.1007/978-3-642-24580-0",
	bibsource = "DBLP, http://dblp.uni-trier.de"
}

Martin Gogolla and Burkhart Wolff (eds.). Tests and Proofs - 5th International Conference, TAP 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings 6706. Springer, 2011.
[ BibTeX ]

@proceedings{DBLP:conf/tap/2011,
	editor = "Martin Gogolla and Burkhart Wolff",
	title = "Tests and Proofs - 5th International Conference, TAP 2011, Zurich, Switzerland, June 30 - July 1, 2011. Proceedings",
	booktitle = "TAP",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 6706,
	year = 2011,
	isbn = "978-3-642-21767-8",
	bibsource = "DBLP, http://dblp.uni-trier.de",
	url = "http://www.lri.fr/~wolff/papers/conf/2011-sacmat-mbtsec-npfit.pdf",
	ee = "http://dx.doi.org/10.1007/978-3-642-21768-5",
	doi = "10.1007/978-3-642-21768-5"
}

Achim D Brucker, Lukas Brügger, Paul Kearney and Burkhart Wolff. An Approach to Modular and Testable Security Models of Real-world Health-Care Applications. Series Proceedings of the ACM Symposium on Access control models and technologies, ACM, 2011, pages 133-142. SACMAT 2011.
[ BibTeX | pdf ]

@incollection{2011-sacmat-mbtsec-npfit,
	author = {Achim D. Brucker and Lukas Br\"ugger and Paul Kearney and Burkhart Wolff},
	title = "An Approach to Modular and Testable Security Models of Real-world Health-Care Applications",
	pages = "133-142",
	publisher = "ACM",
	year = 2011,
	series = "Proceedings of the ACM Symposium on Access control models and technologies",
	abstract = "We present a generic modular policy modelling framework and instantiate it with a substantial case study for model- based testing of some key security mechanisms of applications and services of the NPfIT. NPfIT, the National Programme for IT, is a very large-scale development project aiming to modernise the IT infrastructure of the National Health Service (NHS) in England. Consisting of heteroge- neous and distributed applications, it is an ideal target for model-based testing techniques of a large system exhibiting critical security features. We model the four information governance principles, comprising a role-based access control model, as well as policy rules governing the concepts of patient consent, sealed en- velopes and legitimate relationships. The model is given in Higher-order Logic (HOL) and processed together with suitable test specifications in the HOL-TestGen system, that generates test sequences according to them. Particular em- phasis is put on the modular description of security poli- cies and their generic combination and its consequences for model-based testing.",
	note = "SACMAT 2011",
	doi = "10.1145/1998441.1998461",
	area = "logical_representations",
	pdf = "http://www.brucker.ch/bibliography/download/2011/brucker.ea-model-based-2011.pdf"
}

Abderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff. Isabelle/Circus : a Process Specification and Verification Environment. Number 1547, LRI, http://www.lri.fr/Rapports-internes, November 2011.
[ BibTeX | pdf ]

@techreport{fgw11rapport-lri,
	author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
	title = "Isabelle/Circus : a Process Specification and Verification Environment",
	institution = "LRI, http://www.lri.fr/Rapports-internes",
	year = 2011,
	number = 1547,
	address = "Universit{\'e} Paris-Sud XI",
	month = "November",
	pdf = "http://www.lri.fr/~bibli/Rapports-internes/2011/RR1547.pdf",
	x-equipes = "fortesse",
	x-type = "article",
	x-support = "rapport"
}

Marie-Claude Gaudel. Counting for Random Testing. In Burkhart Wolff and Fatiha Zaidi (eds.). Testing Software and Systems, ICTSS 2011 proceedings 7019. 2011, 1-8.
[ BibTeX | pdf ]

@inproceedings{springerlink:10.1007/978-3-642-24580-0_1,
	author = "Gaudel, Marie-Claude",
	affiliation = "Université Paris-Sud 11, LRI, Orsay, F-91405",
	title = "Counting for Random Testing",
	booktitle = "Testing Software and Systems, ICTSS 2011 proceedings",
	series = "Lecture Notes in Computer Science",
	editor = "Wolff, Burkhart and Zaidi, Fatiha",
	publisher = "Springer Berlin / Heidelberg",
	isbn = "978-3-642-24579-4",
	pages = "1-8",
	volume = 7019,
	year = 2011,
	pdf = "http://www.lri.fr/~mcg/PDF/ICTSS2011gaudel.pdf"
}

Ana Cavalcanti, Marie-Claude Gaudel, Robert Hierons and Manuel Nunez. Conformance Relations for Distributed Testing based on CSP. In Fatiha Zaidi and Burkhart Wolff (eds.). Testing Software and Systems, ICTSS 2011 proceedings 7019. 2011, 48-63.
[ BibTeX ]

@inproceedings{ICTSS:CavGHN2011,
	author = "Ana Cavalcanti and Marie-Claude Gaudel and Robert Hierons and Manuel Nunez",
	title = "Conformance Relations for Distributed Testing based on {CSP}",
	booktitle = "Testing Software and Systems, ICTSS 2011 proceedings",
	volume = 7019,
	series = "Lecture Notes in Computer Science",
	editor = "Fatiha Zaidi and Burkhart Wolff",
	pages = "48-63",
	publisher = "Springer",
	year = 2011
}

Marie-Claude Gaudel. Checking Models, Proving Programs, and Testing Systems. In Martin Gogolla and Burkhart Wolff (eds.). TAP 2011 proceedings 6706. 2011, 1-13.
[ BibTeX | pdf ]

@inproceedings{TAP:Gau2011,
	author = "Marie-Claude Gaudel",
	title = "Checking Models, Proving Programs, and Testing Systems",
	booktitle = "TAP 2011 proceedings",
	volume = 6706,
	series = "Lecture Notes in Computer Science",
	editor = "Martin Gogolla and Burkhart Wolff",
	pages = "1-13",
	publisher = "Springer",
	year = 2011,
	pdf = "http://www.lri.fr/~mcg/PDF/TAP2011gaudel.pdf"
}

Ana Cavalcanti and Marie-Claude Gaudel. Testing for refinement in Circus. Acta Informatica 48(2):97-147, 2011.
[ BibTeX | pdf ]

@article{CavalGau:Acta:2011,
	author = "Ana Cavalcanti and Marie-Claude Gaudel",
	title = "Testing for refinement in {C}ircus",
	journal = "Acta Informatica",
	volume = 48,
	number = 2,
	year = 2011,
	pages = "97-147",
	pdf = "http://www.lri.fr/~mcg/PDF/CavalcantiGaudelCircus221110.pdf"
}

Johan Oudinet, Alain Denise, Marie-Claude Gaudel, Richard Lassaigne and Sylvain Peyronnet. Uniform Monte-Carlo model checking. In Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011 6603. 2011, 127-140.
[ BibTeX | pdf ]

@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 = "Fundamental Approaches to Software Engineering - 14th International Conference, FASE 2011, held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011",
	publisher = "Springer Verlag",
	volume = 6603,
	series = "Lecture Notes in Computer Science",
	year = 2011,
	pages = "127-140",
	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"
}

Mazen El Maarabani, Ana Cavalli, Iksoon Hwang and Fatiha Zaidi. Verification of Interoperability Security Policies By Model Checking. In IEEE (ed.). High Assurance Systems Engineering (HASE). November 2011, 1-7.
[ BibTeX ]

@inproceedings{hase2011,
	author = "Mazen El Maarabani and Ana Cavalli and Iksoon Hwang and Fatiha Zaidi",
	title = "Verification of Interoperability Security Policies By Model Checking",
	booktitle = "High Assurance Systems Engineering (HASE)",
	pages = "1-7",
	year = 2011,
	editor = "IEEE",
	month = "November"
}

Poizat P L. Bentakouk and F Zaidi. Checking the Behavioral Conformance of Web services with Symbolic Testing and an SMT Solver. In Springer (ed.). Tests & Proofs, TAP 6706. July 2011, 33–50.
[ BibTeX ]

@inproceedings{ZF_BPZ11,
	author = "L. Bentakouk, P. Poizat and F. Zaidi",
	title = "Checking the Behavioral Conformance of Web services with Symbolic Testing and an SMT Solver",
	booktitle = "Tests \& Proofs, TAP",
	pages = "33--50",
	year = 2011,
	editor = "Springer",
	volume = 6706,
	series = "LNCS",
	month = "July"
}

Carneiro A Viana, S Maag and F Zaïdi. One step forward: Linking Wireless Self-Organising Networks Validation Techniques with Formal Testing approaches. ACM Computing Survey 43(2):1–39, January 2011.
[ BibTeX ]

@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 = 2011,
	volume = 43,
	number = 2,
	pages = "1--39",
	month = "January"
}

Makarius Wenzel and Burkhart Wolff. Isabelle/PIDE as Platform for Educational Tools. In Pedro Quaresma and Ralph-Johan Back (eds.). Proceedings First Workshop on CTP Components for Educational Software (THedu'11) 79. 2011.
[ BibTeX ]

@inproceedings{Wenzel-Wolff:2011,
	author = "Makarius Wenzel and Burkhart Wolff",
	title = "{Isabelle/PIDE} as Platform for Educational Tools",
	editor = "Pedro Quaresma and Ralph-Johan Back",
	booktitle = "Proceedings First Workshop on CTP Components for Educational Software (THedu'11)",
	series = "EPTCS",
	volume = 79,
	year = 2011
}

M Wenzel. Isabelle as Document-oriented Proof Assistant. In James H Davenport, William M Farmer, Florian Rabe and Josef Urban (eds.). Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011) 6824. 2011.
[ BibTeX ]

@inproceedings{Wenzelm:2011:MKM,
	author = "M. Wenzel",
	title = "Isabelle as Document-oriented Proof Assistant",
	booktitle = "Intelligent Computer Mathematics / Mathematical Knowledge Management (CICM/MKM 2011)",
	year = 2011,
	editor = "James H. Davenport and William M. Farmer and Florian Rabe and Josef Urban",
	volume = 6824,
	series = "LNAI",
	publisher = "Springer"
}

Matthias P Krieger and Achim D Brucker. Extending OCL Operation Contracts with Objective Functions. ECEASST 44, 2011. Proceedings of the International Workshop on OCL and Textual Modelling (OCL 2011).
[ BibTeX ]

@article{objective-functions,
	author = "Matthias P. Krieger and Achim D. Brucker",
	title = "Extending {OCL} Operation Contracts with Objective Functions",
	journal = "ECEASST",
	volume = 44,
	year = 2011,
	note = "Proceedings of the International Workshop on {OCL} and Textual Modelling ({OCL} 2011)"
}

Matthias P Krieger. Test Generation and Animation Based on Object-Oriented Specifications. Phd Thesis, Université Paris-Sud, 2011.
[ BibTeX ]

@phdthesis{krieger-phd,
	author = "Matthias P. Krieger",
	title = "Test Generation and Animation Based on Object-Oriented Specifications",
	school = "Université Paris-Sud",
	year = 2011
}

Paulo Salem Silva. Multi-Agent Systems Verification by Means of Simulation Analysis. Phd Thesis, Université Paris Sud, November 2011. Directeur: Prof. Marie-Claude Gaudel, co-tutelle avec l'Université de Sao Paulo.
[ BibTeX ]

@phdthesis{daSilva2011,
	author = "Paulo Salem da Silva",
	title = "Multi-Agent Systems Verification by Means of Simulation Analysis",
	school = "Universit\'e Paris Sud",
	year = 2011,
	month = "November",
	note = "Directeur: Prof. Marie-Claude Gaudel, co-tutelle avec l'{U}niversit\'e de Sao Paulo",
	x-equipes = "fortesse"
}

Pascal Poizat. Formal Model-Based Approaches for the Development of Composite Systems. HDR, Université Paris Sud, December 2011. Examinateurs: Prof. Philippe Dague, Prof. Marie-Claude Gaudel, Prof. Ernesto Pimentel.
[ BibTeX ]

@phdthesis{poizat2011,
	author = "Pascal Poizat",
	title = "Formal Model-Based Approaches for the Development of Composite Systems",
	school = "Universit\'e Paris Sud",
	year = 2011,
	type = "HDR",
	month = "December",
	note = "Examinateurs: Prof. Philippe Dague, Prof. Marie-Claude Gaudel, Prof. Ernesto Pimentel",
	x-equipes = "fortesse"
}

Matthias Krieger. Test Generation and Animation Based on Object-Oriented Specifications. Phd Thesis, Université Paris Sud, 2011. Directeur de thése: Prof. Burkhart Wolff.
[ BibTeX ]

@phdthesis{krieger2011,
	author = "Matthias Krieger",
	title = "Test Generation and Animation Based on Object-Oriented Specifications",
	school = "Universit\'e Paris Sud",
	year = 2011,
	note = "Directeur de th\'ese: Prof. Burkhart Wolff",
	x-equipes = "fortesse"
}

Lina Bentakouk. Test symbolique de services Web composite. Phd Thesis, Université Paris Sud, 2011. Directeur de thése: Dr. Fatiha Zaidi, Dr. Pascal Poizat.
[ BibTeX ]

@phdthesis{bentakouk2011,
	author = "Lina Bentakouk",
	title = "Test symbolique de services Web composite",
	school = "Universit\'e Paris Sud",
	year = 2011,
	note = "Directeur de th\'ese: Dr. Fatiha Zaidi, Dr. Pascal Poizat",
	x-equipes = "fortesse"
}

Paulo Salem Silva and Ana C V Melo. On-The-Fly Verification of Discrete Event Simulations by Means of Simulation Purposes. In Proceedings of the 2011 Spring Simulation Multiconference (SpringSim'11). 2011.
[ BibTeX ]

@inproceedings{Salem2011b,
	author = "Paulo Salem da Silva and Ana C. V. de Melo",
	title = "On-The-Fly Verification of Discrete Event Simulations by Means of Simulation Purposes",
	booktitle = "Proceedings of the 2011 Spring Simulation Multiconference (SpringSim'11)",
	year = 2011,
	publisher = "The Society for Modeling and Simulation International"
}

Paulo Salem Silva and Ana C V Melo. A Formal Environment Model for Multi-Agent Systems. In Jim Davies, Leila Silva and Adenilso Simao (eds.). Formal Methods: Foundations and Applications. Series Lecture Notes in Computer Science, volume 6527, Springer Berlin / Heidelberg, 2011, pages 64-79.
[ BibTeX ]

@incollection{Salem2011a,
	author = "Paulo Salem da Silva and Ana C. V. de Melo",
	title = "A Formal Environment Model for Multi-Agent Systems",
	booktitle = "Formal Methods: Foundations and Applications",
	series = "Lecture Notes in Computer Science",
	editor = "Davies, Jim and Silva, Leila and Simao, Adenilso",
	publisher = "Springer Berlin / Heidelberg",
	pages = "64-79",
	volume = 6527,
	year = 2011
}

Abderrahmane Feliachi, Marie-Claude Gaudel and Burkhart Wolff. Unifying Theories in Isabelle/HOL. In Unifying Theories of Programming (UTP2010). Series Lecture Notes in Computer Science, volume to appear, number 6445, Springer-Verlag, November 2010, pages 188-206. 20 pages.
[ BibTeX | pdf ]

@incollection{feliachi:uznifying-theories:2010,
	title = "{U}nifying {T}heories in {I}sabelle/{HOL}",
	abstract = "In this paper, we present various extensions of Isabelle/HOL by theories that are essential for several formal methods. First, we explain how we have developed an Isabelle/HOL theory for a part of the Unifying Theories of Programming (UTP). It contains the theories of alphabetized relations and designs. Then we explain how we have encoded first the theory of reactive processes and then the UTP theory for CSP. Our work takes advantage of the rich existing logical core of HOL. Our extension contains the proofs for most of the lemmas and theorems presented in the UTP book. Our goal is to propose a framework that will allow us to deal with formal methods that are semantically based, partly or totally, on UTP, for instance CSP and xsCircus . The theories presented here will allow us to make proofs about such specifications and to apply verified transformations on them, with the objective of assisting refinement and test generation. \keywords{UTP, Theorem Proving, Isabelle/HOL, CSP, Circus}",
	keywords = "UTP, Theorem Proving, Symbolic test case generations, Isabelle/HOL",
	author = "Abderrahmane Feliachi and Marie-Claude Gaudel and Burkhart Wolff",
	booktitle = "Unifying Theories of Programming {(UTP2010)}",
	language = "USenglish",
	publisher = "Springer-Verlag",
	address = "Heidelberg",
	series = "Lecture Notes in Computer Science",
	number = 6445,
	classification = "conference",
	ee = "http://dx.doi.org/10.1007/978-3-642-16690-7_9",
	year = 2010,
	doi = "10.1007/978-3-642-16690-7_9",
	pdf = "http://www.lri.fr/~wolff/papers/conf/2010-utp-unifying-theories.pdf",
	area = "logical_representations",
	public = "yes",
	volume = "to appear",
	month = "November",
	note = "20 pages",
	x-equipes = "fortesse",
	x-type = "article",
	x-support = "actes",
	x-cle-support = "B",
	type_digiteo = "conf_isbn",
	pages = "188-206"
}

Achim D Brucker, Matthias P Krieger, Delphine Longuet and Burkhart Wolff. A Specification-based Test Case Generation Method for UML/OCL. In Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010) 6627. 2010. LNCS 6627.
[ BibTeX | pdf ]

@inproceedings{Brucker.ea:SpecificationBased:2010,
	author = "Achim D. Brucker and Matthias P. Krieger and Delphine Longuet and Burkhart Wolff",
	title = "{A} {S}pecification-based {T}est {C}ase {G}eneration {M}ethod for {UML}/{OCL}",
	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 repre- sentation 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",
	booktitle = "Proceedings of the Workshop on OCL and Textual Modelling (OCL 2010)",
	classification = "conference",
	year = 2010,
	doi = "10.1007/978-3-642-21210-9_33",
	area = "logical_representations",
	note = "LNCS 6627",
	publisher = "Springer",
	series = "Lecture Notes in Computer Science",
	volume = 6627
}

Matthias P Krieger, Alexander Knapp and Burkhart Wolff. Automatic and Efficient Simulation of Operation Contracts. In Eelco Visser, Jaakko Jarvi and Giorgios Economopoulos (eds.). Ninth International Conference on Generative Programming and Component Engineering (GPCE'10). 2010.
[ BibTeX | pdf ]

@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",
	isbn = "978-1-4503-0154-1",
	doi = "10.1145/1868294.1868303",
	classification = "conference",
	pdf = "http://www.lri.fr/~wolff/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."
}

Achim D Brucker, Lukas Brügger, Paul Kearney and Burkhart Wolff. Verified Firewall Policy Transformations for Test Case Generation. Software Testing, Verification, and Validation, 2010 International Conference on 0:345-354, 2010.
[ BibTeX | pdf ]

@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",
	area = "logical_representations",
	pdf = "http://www.lri.fr/~wolff/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."
}

Achim D Brucker, Lukas Brügger, Matthias P Krieger and Burkhart Wolff. HOL-TestGen 1.5.0 User Guide. Number 670, ETH Zurich, April 2010.
[ BibTeX | pdf ]

@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",
	year = 2010
}

Abderrahmane Feliachi and Hélène LeGuen. Generating transition probabilities for automatic model-based test generation. In International Conference on Software Testing, Verification and Validation (ICST). April 2010, 99–102.
[ BibTeX | pdf ]

@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"
}

Abderrahmane Feliachi. Tests generation from Circus specifications. In MOdelling and VErifying parallel Processes (MOVEP). June 2010, 70–75.
[ BibTeX ]

@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"
}

Ana Cavalcanti and Marie-Claude Gaudel. Specification coverage for testing in Circus. In Unifying Theories of Programming 2010 6445. November 2010, 1-45.
[ BibTeX | 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 = 6445,
	series = "Lecture Notes in Computer Science",
	month = "November",
	year = 2010,
	pages = "1-45",
	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"
}

Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel and Jim Woodcock (eds.). Theoretical Aspects of Computing - ICTAC 2010, 7th International Colloquium, Natal, Rio Grande do Norte, Brazil, September 1-3, 2010. Proceedings 6255. Springer, 2010.
[ BibTeX ]

@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
}

Johan Oudinet, Alain Denise and Marie-Claude Gaudel. A new dichotomic algorithm for the uniform random generation of words in regular languages. In Conference on random and exhaustive generation of combinatorial objects (GASCom). September 2010. 10 pages.
[ BibTeX ]

@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 = "UQAM"
}

Marie-Claude Gaudel. Software Testing Based on Formal Specification. In Paulo Borba, Ana Cavalcanti, Augusto Sampaio and Jim Woodcock (eds.). Testing Techniques in Software Engineering, Second Pernambuco Summer School on Software Engineering, PSSE 2007, December 3-7, 2007, Revised Lectures 6153. 2010, 215-242.
[ BibTeX ]

@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
}

Fatiha Zaidi, Mounir Lallali and Stephane Maag. A Component based Testing Technique for a Manet Routing Protocol. In AICCSA'2010 - ACS/IEEE International Conference on Computer Sustems and Applications. May 2010, 1–7.
[ BibTeX ]

@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"
}

A Cavalli, T-D Cao, W Mallouli, E Martins, A Sadovykh, S Salva and F Zaidi. WebMov : A Dedicated Framework for the Modelling and Testing of Web Services. In ICWS 2010 - IEEE International Conference on Web Services. July 2010, 377–384.
[ BibTeX ]

@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"
}

A Carneiro, T Herault, T Largillier, S Peyronnet and F Zaidi. Supple: A Flexible Probabilistic Data Dissemination Protocol for Wireless Sensor Networks. In MSWIM'2010 - The 13th ACM International Conference on Modeling Analysis and Simulation of Wireless and Mobile Systems. October 2010, 385–393.
[ BibTeX ]

@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"
}

A Cavalli, M Lallali, S Maag, G Morales and F Zaidi. Emergent Web Intelligence. Series Advanced Information and Knowledge Processing, chapter Modeling and Testing of Web Based Systems: Advanced Semantic Technologies, pages 355–392, Springer Verlag, 2010.
[ BibTeX ]

@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"
}

D Matthews and M Wenzel. Efficient Parallel Programming in Poly/ML and Isabelle/ML. In ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming (DAMP 2010). 2010.
[ BibTeX ]

@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
}

Makarius Wenzel. Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In Sacerdoti C Coen and D Aspinall (eds.). User Interfaces for Theorem Provers (UITP 2010). July 2010. FLOC 2010 Satellite Workshop.
[ BibTeX ]

@inproceedings{wenzel:2010,
	author = "Makarius Wenzel",
	title = "Asynchronous Proof Processing with {Isabelle/Scala} and {Isabelle/jEdit}",
	booktitle = "User Interfaces for Theorem Provers (UITP 2010)",
	year = 2010,
	editor = "C. Sacerdoti Coen and D. Aspinall",
	series = "ENTCS",
	month = "July",
	note = "FLOC 2010 Satellite Workshop"
}

Delphine Longuet, Marc Aiguier and Pascale Le Gall. Proof-guided test selection from quantifier-free first-order specifications with equality. Journal of Automated Reasoning, special issue on Tests and Proofs 45(4):437-473, 2010.
[ BibTeX | pdf ]

@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"
}

Marc Aiguier and Delphine Longuet. Some general results about proof normalization. Logica Universalis 4(1):1-29, 2010.
[ BibTeX | pdf ]

@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"
}

Johan Oudinet. Approches combinatoires pour le test statistique a grande échelle. Phd Thesis, Université Paris Sud, November 2010. Directeur: Prof. Marie-Claude Gaudel.
[ BibTeX ]

@phdthesis{oudinet2010,
	author = "Johan Oudinet",
	title = "Approches combinatoires pour le test statistique a grande \'echelle",
	school = "Universit\'e Paris Sud",
	year = 2010,
	month = "November",
	note = "Directeur: Prof. Marie-Claude Gaudel",
	x-equipes = "fortesse"
}

Burkhart Wolff. Top-down vs. Bottom-up: Formale Methoden im wissenschaftlichen Wettbewerb. Ein essayistischer Survey über den Stand der Kunst.. DFKI Technischer Bericht, 2009. Erschienen in der Festschrift zum 60. Geburtstag von Bernd Krieg-Brückner..
[ BibTeX | pdf ]

@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 versus Bottom-up oder post-hoc Programmverifikation --- Bereich “For- maler Methoden” zu geben. Als Einordnungsrahmen benutze ich Lakatos'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.}
}

Sascha Böhme, Michał Moskal, Wolfram Schulte and Burkhart Wolff. HOL-Boogie –- An Interactive Prover-Backend for the Verified C Compiler. Journal of Automated Resoning (JAR) 44(1–2):111–144, 2009.
[ BibTeX | 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 = "http://www.lri.fr/~wolff/papers/journals/hol-boogie.pdf",
	keywords = "Isabelle/HOL, Theorem proving, Program verification, Memory models, Annotation languages",
	classification = "journal"
}

Achim D Brucker and Burkhart Wolff. Semantics, Calculi, and Analysis for Object-Oriented Specifications. Acta Informatica 46(4):255–284, 2009.
[ BibTeX | pdf ]

@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 = "http://www.lri.fr/~wolff/papers/journals/acta-holocl.pdf",
	keywords = "UML , OCL , object-oriented specification , refinement , formal methods",
	doi = "10.1007/s00236-009-0093-8",
	area = "logical_representations",
	classification = "journal"
}

Matthias Daum, Jan Dörrenbächer and Burkhart Wolff. Proving Fairness and Implementation Correctness of a Microkernel Scheduler. Journal of Automated Reasoning (JAR) 42(2–4):349–388, 2009. G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2008)..
[ BibTeX | 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 = "http://www.lri.fr/~wolff/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",
	area = "logical_representations",
	classification = "journal"
}

Achim D Brucker and Burkhart Wolff. HOL-TestGen: An Interactive Test-case Generation Framework. In Marsha Chechik and Martin Wirsing (eds.). Fundamental Approaches to Software Engineering (FASE09). Series Lecture Notes in Computer Science, number 5503, Springer-Verlag, 2009, pages 417–420.
[ BibTeX | pdf ]

@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"
}

Achim D Brucker, Matthias P Krieger and Burkhart Wolff. Extending OCL with Null-References. In S Ghosh (ed.). MODELS 2009 Workshops. Series LNCS 6002, Springer Verlag, Heidelberg, 2009, pages 261–275. Best-Paper Award at the OCL 2009 Workshop..
[ BibTeX | pdf ]

@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.",
	ee = "http://dx.doi.org/10.1007/978-3-642-12261-3_25",
	doi = "10.1007/978-3-642-12261-3_25"
}

M -C Gaudel, F Magnez, R Lassaigne and M Rougemont. Approximations for Model Checking and Testing (survey, preliminary version). 39 pages, under revision, Université de Paris-Sud, May 2009.
[ BibTeX | 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"
}

L Bentakouk, P Poizat and F Zaïdi. A Formal Framework for Service Orchestration Testing based on Symbolic Transition Systems. In TESTCOM/FATES 2009 - 21th IFIP International Conference on Testing of Communicating Systems 5826. November 2009, 16–32.
[ BibTeX ]

@inproceedings{testcom09,
	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"
}

F Zaïdi, A Cavalli and E Bayse. NetworkProtocol Interoperability Testing based on Contextual. In 24th Annual ACM Symposium on Applied on Applied Computing. March 2009, 2–7.
[ BibTeX ]

@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"
}

A Cavalli, S Maag, Montes E Oca and F Zaidi. A Formal Passive Testing Approach to test a MANET Routing Protocol. In PWN 2009 5th IEEE PerCom Workshop on Pervasive Wireless Networking. March 2009, 1–6.
[ BibTeX ]

@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"
}

Florian Haftmann and Makarius Wenzel. Local theory specifications in Isabelle/Isar. In Stefano Berardi, Ferruccio Damiani and Ugo Liguoro (eds.). Types for Proofs and Programs, TYPES 2008 5497. 2009.
[ BibTeX ]

@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 = "LNCS",
	volume = 5497,
	year = 2009
}

Norbert Schirmer and Makarius Wenzel. State Spaces –- The Locale Way. In Ralf Huuck, Gerwin Klein and Bastian Schlich (eds.). Systems Software Verification (SSV 2009). 2009.
[ BibTeX ]

@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"
}

M Wenzel. Parallel Proof Checking in Isabelle/Isar. In G Dos Reis and L Théry (eds.). ACM SIGSAM Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS 2009). 2009.
[ BibTeX ]

@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"
}

Delphine Longuet and Marc Aiguier. Integration Testing from Structured First-Order Specifications via Deduction Modulo. In International Conference Theoretical Aspects of Computing (ICTAC 2009) 5684. 2009, 261-276.
[ BibTeX | pdf ]

@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"
}

Johan Oudinet. Exploration aléatoire de modèles. Journal Européen des Systèmes Automatisés (JESA) 43:905–919, November 2009. Colloque francophone sur la Modélisation des Systèmes Réactifs.
[ BibTeX | pdf ]

@article{oudinetJESA09,
	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://rukia.lri.fr/publis/JESA09.pdf"
}

Paulo Salem Silva. An Environment Specification Language for Multi-Agent Systems. 2009. Technical Report 1531 – Universit� Paris-Sud 11, Laboratoire de Recherche en Informatique.
[ BibTeX ]

@techreport{Salem2009,
	author = "Paulo Salem da Silva",
	title = "An Environment Specification Language for Multi-Agent Systems",
	note = "Technical Report 1531 -- Universit� Paris-Sud 11, Laboratoire de Recherche en Informatique",
	year = 2009
}

Sascha Böhme, Rustan Leino and Burkhart Wolff. HOL-Boogie –- An Interactive Prover for the Boogie Program Verifier. In Sofiene Tahar, Otmane Ait Mohamed and César Muñoz (eds.). 21th International Conference on Theorem proving in Higher-Order Logics (TPHOLs 2008). Series LNCS 5170, Springer-Verlag, 2008.
[ BibTeX | pdf ]

@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 provers such 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.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"
}

Achim D Brucker and Burkhart Wolff. An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. Journal of Automated Reasoning (JAR) 41(3–4):219-249, 2008. Serge Autexier, Heiko Mantel, Stephan Merz, and Tobias Nipkow (eds).
[ BibTeX | pdf ]

@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.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 = 41,
	doi = "10.1007/s10817-008-9108-3",
	pages = "219-249",
	number = "3--4",
	year = 2008
}

Achim D Brucker and Burkhart Wolff. Extensible Universes for Object-Oriented Data Models. In Jan Vitek (ed.). Proceedings of the European Conference of Object-Oriented Programming (ECOOP 2008). Series LNCS 5142, Springer-Verlag, July 2008, pages 438–462.
[ BibTeX | pdf ]

@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.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"
}

Achim D Brucker and Burkhart Wolff. A Formal Proof Environment for UML/OCL. In Proceedings of Formal Aspects of Software Engineering (FASE 2008) 4961. 2008, 97–101.
[ BibTeX | pdf ]

@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
}

Achim D Brucker, Lukas Brügger and Burkhart Wolff. Model-based Firewall Conformance Testing. In Kenji Suzuki and Teruo Higashino (eds.). Testcom/FATES 2008. Series LNCS 5047, Springer-Verlag, 2008, pages 103–118.
[ BibTeX | pdf ]

@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.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"
}

Achim D Brucker, Lukas Brügger and Burkhart Wolff. Verifying Test-Hypotheses – An Experiment in Test and Proof. In Bernd Finkbeiner, Yuri Gurevich and Alexander K Petrenko (eds.). Model-based Testing (MBT) 2008 202. 2008, 15-28.
[ BibTeX | pdf ]

@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.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"
}

Matthias Daum, Jan Dörrenbächer, Mareike Schmidt and Burkhart Wolff. A Verification Approach for System-Level Concurrent Programs. In Verified Software: Theories, Tools, Experiments. Series LNCS 5295, Springer Berlin / Heidelberg, September 2008, pages 161–176.
[ BibTeX | pdf ]

@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.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"
}

Marie-Claude Gaudel, Alain Denise, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet and Sylvain Peyronnet. Coverage-biased random exploration of large models. In 4th ETAPS Workshop on Model Based Testing 220, Issue 1, 10. March 2008, 3-14. invited lecture.
[ BibTeX | pdf ]

@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 = "4th ETAPS Workshop on Model Based Testing",
	series = "Electronic Notes in Theoretical Computer Science",
	year = 2008,
	volume = "220, Issue 1, 10",
	pages = "3-14",
	x-equipes = "fortesse bioinfo parall EXT",
	x-type = "invitation",
	x-support = "actes",
	x-cle-support = "B",
	note = "invited lecture",
	pdf = "http://www.lri.fr/~mcg/PDF/MBT08.pdf",
	month = "March"
}

Ana Cavalcanti and Marie-Claude Gaudel. A note on traces refinement and the {\textitconf} relation in the Unifying Theories of Programming. In Andrew Butterfield (ed.). Unifying Theories of Programming, Second International Symposium, UTP 2008, Trinity College, Dublin, Ireland, September 8-10, 2008, Revised Selected Papers 5713. 2008, 42–61.
[ BibTeX | pdf ]

@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"
}

M Lallali, F Zaidi, A Cavalli and I Hwang. Automatic Timed Test Case Generation for Web Services Composition. In IEEE Computer Society Press (ed.). The 6th IEEE European Conference on Web Services (ECOWS'08). November 2008. 53–63.
[ BibTeX | pdf ]

@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"
}

M Lallali, F Zaidi and A Cavalli. Transforming BPEL into Intermediate Format Language For Web Services Composition Testing. In 4th International Conference on Next Generation Web Services Practices. October 2008. 191–197.
[ BibTeX | pdf ]

@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"
}

Stefan Berghofer and Makarius Wenzel. Logic-free reasoning in Isabelle/Isar. In Intelligent Computer Mathematics –- Mathematical Knowledge Management (MKM 2008) 5144. 2008.
[ BibTeX ]

@inproceedings{Berghofer-Wenzel:2008,
	author = "Stefan Berghofer and Makarius Wenzel",
	title = "Logic-free reasoning in {Isabelle/Isar}",
	booktitle = "Intelligent Computer Mathematics --- Mathematical Knowledge Management (MKM 2008)",
	year = 2008,
	series = "",
	volume = 5144,
	publisher = "Springer"
}

M Wenzel, L C Paulson and T Nipkow. The Isabelle Framework. In Theorem Proving in Higher Order Logics (TPHOLs 2008). 2008. Invited paper.
[ BibTeX ]

@inproceedings{Wenzel-Paulson-Nipkow:2008,
	author = "M. Wenzel and L.C. Paulson and T. Nipkow",
	title = "The {Isabelle} Framework",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 2008)",
	series = "LNCS",
	year = 2008,
	note = "Invited paper",
	publisher = "Springer",
	url = "http://www4.in.tum.de/~wenzelm/papers/isabelle-overview.pdf"
}

Mohammad Mahdi Jaghoori, Delphine Longuet and Frank S Boer. Schedulability and Compatibility of Real-Time Asynchronous Objects. In 29th IEEE Real-Time Systems Symposium (RTSS 2008). 2008, 70-79.
[ BibTeX | pdf ]

@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"
}

Alain Denise, Marie-Claude Gaudel, Sandrine-Dominique Gouraud, Richard Lassaigne, Johan Oudinet and Sylvain Peyronnet. Coverage-Biased Random Exploration of Large Models and Application to Testing. Number 1494, LRI, June 2008.
[ BibTeX | pdf ]

@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"
}

Johan Oudinet. Uniform Random Exploration of Concurrent Systems. In MOdelling and VErifying parallel Processes (MOVEP). June 2008, 323–328.
[ BibTeX ]

@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"
}

J Fayolle, M -C Gaudel, S -D Gouraud and B Marre. Statistical Testing of Synchronous Reactive Systems. In ERTS. 2008.
[ BibTeX ]

@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"
}

David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi and Burkhart Wolff. Verifying a signature architecture: a comparative case study. Formal Aspects of Computing 19(1):63–91, March 2007. http://www.springerlink.com/content/u368650p18557674/?p=8851693f5ba14a3fb9d493dae37783b8&pi=0.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications/papers/2007/fac.submit.pdf",
	title = "Verifying a signature architecture: a comparative case study",
	volume = 19,
	year = 2007,
	user = "lukasbru"
}

David Basin, Hironobu Kuruma, Shin Nakajima and Burkhart Wolff. The Z Specification Language and the Proof Environment Isabelle/HOL-Z. Computer Software –- Journal of the Japanese Society for Software Science and Technology 24(2):21–26, April 2007. In Japanese..
[ BibTeX ]

@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"
}

Achim D Brucker, Jürgen Doser and Burkhart Wolff. An MDA Framework Supporting OCL. Electronic Communications of the EASST 5, 2007.
[ BibTeX | pdf ]

@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.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"
}

Achim D Brucker, Jürgen Doser and Burkhart Wolff. Semantic Issues of OCL: Past, Present, and Future. Electronic Communications of the EASST 5, 2007.
[ BibTeX | pdf ]

@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.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"
}

Achim D Brucker and Burkhart Wolff. Test-Sequence Generation with HOL-TestGen – With an Application to Firewall Testing. In Bertrand Meyer and Yuri Gurevich (eds.). TAP 2007: Tests And Proofs. Series lncs, number 4454, Springer-Verlag, 2007, pages 149–168.
[ BibTeX | 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 = "lncs",
	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",
	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"
}

Makarius Wenzel and Burkhart Wolff. Building Formal Method Tools in the Isabelle/Isar Framework. In Klaus Schneider and Jens Brandt (eds.). TPHOLs 2007. Series LNCS 4732, Springer-Verlag, 2007, pages 351–366.
[ BibTeX | 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.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"
}

Nicolas Baskiotis, Michèle Sebag, Marie-Claude Gaudel and Sandrine-Dominique Gouraud. A Machine Learning Approach for Statistical Software Testing. In IJCAI, Proceedings of the 20th International Joint Conference on Artificial Intelligence. 2007, 2274-2279.
[ BibTeX | 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",
	type_digiteo = "conf_isbn"
}

A Cavalcanti and M -C Gaudel. Testing for Refinement in CSP. In Formal Methods and Software Engineering, ICFEM 2007 4789. 2007, 151-170.
[ BibTeX | pdf ]

@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"
}

M -C Gaudel and Le P Gall. Testing Data Types Implementations from Algebraic Specifications. In Formal Methods and Testing, R. Hierons, J. Bowen, and M. Harman,eds. Series Lecture Notes in Computer Science, volume 4949, Springer-Verlag, 2007. 209-239.
[ BibTeX | pdf ]

@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"
}

M Lallali, F Zaidi and A Cavalli. Timed Modeling of Web Services Composition for Automatic Testing. In SITIS IEEE/ACM 2007. December 2007, 417–427.
[ BibTeX | 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"
}

F Zaidi and Mounir Lallali. Use of Verification Techniques for Components Testing. Number 1465, LRI, http://www.lri.fr/Rapports-internes, January 2007.
[ BibTeX ]

@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"
}

M Lallali, F Zaidi and A Cavalli. Timed Modeling of Web Services Composition for Automatic Testing. Number 07008-LOR, GET/INT, September 2007. Long version.
[ BibTeX ]

@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"
}

Amine Chaieb and Makarius Wenzel. Context aware Calculation and Deduction –- Ring Equalities via Gröbner Bases in Isabelle. In Manuel Kauers, Manfred Kerber, Robert Miner and Wolfgang Windsteiger (eds.). Towards Mechanized Mathematical Assistants (CALCULEMUS 2007) 4573. 2007.
[ BibTeX ]

@inproceedings{Chaieb-Wenzel:2007,
	author = "Amine Chaieb and Makarius Wenzel",
	title = {Context aware Calculation and Deduction --- Ring Equalities via {Gr\"obner Bases} in {Isabelle}},
	booktitle = "Towards Mechanized Mathematical Assistants (CALCULEMUS 2007)",
	editor = "Manuel Kauers and Manfred Kerber and Robert Miner and Wolfgang Windsteiger",
	series = "LNAI",
	volume = 4573,
	year = 2007,
	publisher = "Springer"
}

Florian Haftmann and Makarius Wenzel. Constructive Type Classes in Isabelle. In T Altenkirch and C McBride (eds.). Types for Proofs and Programs (TYPES 2006) 4502. 2007.
[ BibTeX ]

@inproceedings{Haftmann-Wenzel:2006,
	author = "Florian Haftmann and Makarius Wenzel",
	title = "Constructive Type Classes in {Isabelle}",
	editor = "T. Altenkirch and C. McBride",
	booktitle = "Types for Proofs and Programs (TYPES 2006)",
	series = "LNCS",
	volume = 4502,
	year = 2007,
	publisher = "Springer"
}

Makarius Wenzel and Amine Chaieb. SML with antiquotations embedded into Isabelle/Isar. In Jacques Carette and Freek Wiedijk (eds.). Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007). Hagenberg, Austria. June 2007.
[ BibTeX ]

@inproceedings{Wenzel-Chaieb:2007b,
	author = "Makarius Wenzel and Amine Chaieb",
	title = "{SML} with antiquotations embedded into {Isabelle/Isar}",
	booktitle = "Workshop on Programming Languages for Mechanized Mathematics (PLMMS 2007). Hagenberg, Austria",
	editor = "Jacques Carette and Freek Wiedijk",
	month = "June",
	year = 2007
}

M Wenzel and B Wolff. Building Formal Method Tools in the Isabelle/Isar Framework. In K Schneider and J Brandt (eds.). Theorem Proving in Higher Order Logics (TPHOLs 2007) 4732. 2007.
[ BibTeX ]

@inproceedings{Wenzel-Wolff:2007,
	author = "M. Wenzel and B. Wolff",
	title = "Building Formal Method Tools in the {Isabelle/Isar} Framework",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 2007)",
	editor = "K. Schneider and J. Brandt",
	series = "LNCS",
	volume = 4732,
	year = 2007,
	publisher = "Springer"
}

Makarius Wenzel. Isabelle/Isar –- a generic framework for human-readable proof documents. In R Matuszewski and A Zalewska (eds.). From Insight to Proof –- Festschrift in Honour of Andrzej Trybulec. Series Studies in Logic, Grammar, and Rhetoric, volume 10(23), University of Białystok, 2007.
[ BibTeX ]

@incollection{Wenzel:2006:Festschrift,
	author = "Makarius Wenzel",
	title = "{Isabelle/Isar} --- a generic framework for human-readable proof documents",
	booktitle = "From Insight to Proof --- Festschrift in Honour of Andrzej Trybulec",
	publisher = "University of Bia{\l}ystok",
	year = 2007,
	editor = "R. Matuszewski and A. Zalewska",
	volume = "10(23)",
	series = "Studies in Logic, Grammar, and Rhetoric",
	url = "\url{http://www.in.tum.de/~wenzelm/papers/isar-framework.pdf}"
}

Delphine Longuet. Test à partir de spécifications axiomatiques. Phd Thesis, Laboratoire IBISC, Université d'Évry-Val d'Essonne, 2007.
[ BibTeX | pdf ]

@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"
}

Marc Aiguier and Delphine Longuet. Test Selection Criteria for Modal Specifications of Reactive Systems. In First Joint IEEE/IFIP Symposium on Theoretical Aspects of Software Engineering (TASE 2007). 2007, 159-170.
[ BibTeX | 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"
}

Marc Aiguier, Agnès Arnould, Pascale Le Gall and Delphine Longuet. Test Selection Criteria for Quantifier-Free First-Order Specifications. In International Symposium on Fundamentals of Software Engineering (FSEN 2007) 4767. 2007, 144-159.
[ BibTeX | pdf ]

@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"
}

Delphine Longuet and Marc Aiguier. Specification-Based Testing for CoCasl's Modal Specifications. In Second International Conference on Algebra and Coalgebra in Computer Science (CALCO 2007) 4624. 2007, 356-371.
[ BibTeX | 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"
}

Johan Oudinet. Uniform random walks in concurrent models. Masters Thesis, Université Paris-Sud 11, LRI, September 2007.
[ BibTeX | 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"
}

Johan Oudinet. Tirages aléatoires uniformes dans des systèmes concurrents. Masters Thesis, Université Paris-Sud 11, LRI, September 2007.
[ BibTeX | 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."
}

Johan Oudinet. Uniform Random Walks in Very Large Models. In RT '07: Proceedings of the 2nd international workshop on Random testing. November 2007, 26–29.
[ BibTeX | pdf ]

@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."
}

Achim D Brucker and Burkhart Wolff. The HOL-OCL Book. Number 525, ETH Zürich, 2006.
[ BibTeX | 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"
}

Achim D Brucker, Jürgen Doser and Burkhart Wolff. An MDA Framework Supporting OCL. In 6th OCL Workshop at the UML/MoDELS Conference. 2006.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications/papers/2006/OclApps-framework.pdf",
	title = "An {MDA} Framework Supporting{ OCL}",
	classification = "workshop",
	year = 2006,
	user = "wolff"
}

Achim D Brucker, Jürgen Doser and Burkhart Wolff. A Model Transformation Semantics and Analysis Methodology for SecureUML. In Oscar Nierstrasz, Jon Whittle, David Harel and Gianna Reggio (eds.). MoDELS 2006: Model Driven Engineering Languages and Systems. Series LNCS 4199, Springer-Verlag, 2006, pages 306–320. An extended version of this paper is available as ETH Technical Report, no. 524..
[ BibTeX | pdf ]

@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"
}

Achim D Brucker and Burkhart Wolff. A Package for Extensible Object-Oriented Data Models with an Application to IMP++. In Abhik Roychoudhury and Zijiang Yang (eds.). International Workshop on Software Verification and Validation (SVV 2006). Series Computing Research Repository (CoRR), 2006.
[ BibTeX | pdf ]

@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 = "",
	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"
}

Achim D Brucker, Jürgen Doser and Burkhart Wolff. Semantic Issues of OCL: Past, Present, and Future. In 6th OCL Workshop at the UML/MoDELS Conference. 2006.
[ BibTeX | pdf ]

@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.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"
}

Manuel Núñez Garc\'\ia, Klaus Havelund, Grigore Rosu and Burkhart Wolff (eds.). Proceedings of the International Workshop on Formal Aspects of Testing and Runtime Verification (FATES/RV). Springer Verlag, Seattle, USA, 2006. LNCS 4262..
[ BibTeX ]

@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"
}

A Denise, M -C Gaudel, S -D Gouraud, R Lasseigne and S Peyronnet. Uniform Random Sampling of Traces in very Large Models. In 1st International ACM Workshop on Random Testing. July 2006, 10 -19.
[ BibTeX | 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"
}

M -C Gaudel. Validation et Vérification. In Encyclopédie de l'informatique et des systèmes d'information. Vuibert, 2006, pages 1136-1150.
[ BibTeX ]

@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"
}

M -C Gaudel. Les objets à l'épreuve des faits. In Communication, Connaissance : supports et médiations à l'âge de l'information, J.-G. Ganascia, ed.. CNRS Éditions, 2006. 4 pages.
[ BibTeX ]

@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"
}

G Lestiennes and M -C Gaudel. Modélisation et Test de Systèmes comportant des actions prioritaires. Rapport LRI 1434, Université de Paris-Sud, March 2006.
[ BibTeX | pdf ]

@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"
}

S Maag and F Zaidi. A Step-Wise Validation Approach for a Wireless Routing Protocol. In IEEE International Conference on Communications and Electronics (ICCE'06). October 2006.
[ BibTeX ]

@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"
}

S Maag and F Zaidi. Testing methodology for an ad hoc routing protocol. In PM2HW2N '06: Proceedings of the ACM international workshop on Performance monitoring, measurement, and evaluation of heterogeneous wireless and wired networks. 2006, 48–55. http://doi.acm.org/10.1145/1163653.1163663.
[ BibTeX | pdf ]

@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"
}

S Maag and F Zaidi. Spécification Formelle pour le Test d'un Protocole de Routage ad hoc. Number 06009-LOR, GET/INT, October 2006.
[ BibTeX ]

@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"
}

Markus Wenzel and Lawrence C Paulson. Isabelle/Isar. In F Wiedijk (ed.). The Seventeen Provers of the World. Series LNAI, volume 3600, Springer, 2006.
[ BibTeX ]

@incollection{Wenzel-Paulson:2006,
	author = "Markus Wenzel and Lawrence C. Paulson",
	title = "{Isabelle/Isar}",
	booktitle = "The Seventeen Provers of the World",
	year = 2006,
	editor = "F. Wiedijk",
	series = "LNAI",
	volume = 3600,
	publisher = "Springer"
}

Makarius Wenzel. Structured Induction Proofs in Isabelle/Isar. In J Borwein and W Farmer (eds.). Mathematical Knowledge Management (MKM 2006) 4108. 2006.
[ BibTeX ]

@inproceedings{Wenzel:2006,
	author = "Makarius Wenzel",
	title = "Structured Induction Proofs in {Isabelle/Isar}",
	booktitle = "Mathematical Knowledge Management (MKM 2006)",
	year = 2006,
	editor = "J. Borwein and W. Farmer",
	series = "LNAI",
	volume = 4108,
	publisher = "Springer"
}

Marc Aiguier, Diane Bahrami and Delphine Longuet. An Abstract Way to Define Rewriting Logic. In IPM International Workshop on Foundations of Software Engineering (FSEN 2005) 159. 2006, 205-226.
[ BibTeX | pdf ]

@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"
}

A Denise, M -C Gaudel, S -D Gouraud, R Lassaigne and S Peyronnet. Uniform Random Sampling of Traces in Very Large Models. In 1st ACM International Workshop on Random Testing (RT). 2006, 10-19.
[ BibTeX ]

@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"
}

S -D Gouraud and A Gotlieb. Using CHRs to generate functional test cases for the Java Card Virtual Machine. In 8th International Symposium on Practical Aspects of Declarative Languages (PADL). 2006, 1-15.
[ BibTeX | pdf ]

@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"
}

A Denise, M -C Gaudel, S -D Gouraud, R Lassaigne and S Peyronnet. Uniform Random Sampling of Traces in Very Large Models. Number 1445, 2006.
[ BibTeX | pdf ]

@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"
}

David Aspinall, Christoph Lüth and Burkhart Wolff. Assisted Proof Document Authoring. In Fourth International Conference on Mathematical Knowledge Management (MKM 05). Series LNCS 3863., Springer Verlag, 2005.
[ BibTeX | 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"
}

David Basin, Hironobu Kuruma, Kazuo Takaragi and Burkhart Wolff. Specifying and Verifying Hysteresis Signature System with HOL-Z. Number 471, Computer Security Group, ETH Zürich, January 2005.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications-softech/papers/2005/HSD.pdf",
	title = "{S}pecifying and {V}erifying {H}ysteresis {S}ignature {S}ystem with {HOL-Z}",
	year = 2005,
	user = "wolff"
}

David Basin, Hironobu Kuruma, Kazuo Takaragi and Burkhart Wolff. Verification of a Signature Architecture with HOL-Z. In Formal Methods 2005. Series LNCS 3582, Springer Verlag, 2005, pages 269–285.
[ BibTeX | pdf ]

@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"
}

Achim D Brucker and Burkhart Wolff. HOL-TestGen 1.0.0 User Guide. Number 482, Computer Security Group, ETH Zürich, April 2005.
[ BibTeX ]

@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"
}

Achim D Brucker and Burkhart Wolff. Interactive Testing using HOL-TestGen. In Wolfgang Grieskamp and Carsten Weise (eds.). Formal Approaches to Testing of Software (FATES 05). Series LNCS 3997, Springer-Verlag, 2005, pages 87–102.
[ BibTeX ]

@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"
}

Achim D Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. In Jens Grabowski and Brian Nielsen (eds.). Formal Approaches to Testing of Software (FATES 04). Series LNCS 3395, Springer-Verlag, 2005, pages 16–32.
[ BibTeX ]

@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"
}

Achim D Brucker and Burkhart Wolff. A Verification Approach for Applied System Security. International Journal on Software Tools for Technology Transfer (STTT) 7(3):233–247, 2005.
[ BibTeX | pdf ]

@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.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"
}

Thomas Meyer and Burkhart Wolff. Tactic-based Optimized Compilation of Functional Programs. In Jean-Christophe Filliatre, Christine Paulin and Benjamin Werner (eds.). Types for Proofs and Programs (TYPES 2004). Series LNCS 3839, Springer Verlag, August 2005, pages 202–215.
[ BibTeX | 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.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"
}

M -C Gaudel. Formal Methods and Testing: Hypotheses, and Correctness Approximations. In FM 2005: Formal Methods: International Symposium of Formal Methods 3582. 2005, 2-8. keynote talk.
[ BibTeX | 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"
}

G Lestiennes and M -C Gaudel. Test de systèmes réactifs non réceptifs. Journal Europén des Systèmes automatisés 36(1-2-3):255-270, 2005. proceedings of MSR'05.
[ BibTeX | pdf ]

@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"
}

M -C Gaudel. Toward Undoing in Composite Web Services. In Architecting Dependable Systems III 3549. 2005, 59-68.
[ BibTeX | 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"
}

C Jones, D Lomet, A Romanovsky, G Weikum, A Fekete, M -C Gaudel, H F Korth, R Lemos, E Moss, R Rajwar, K Ramamritham, B Randell and L Rodrigues. The Atomic Manifesto: a Story in Four Quarks. Journal of Universal Computer Science 11(5):636-650, 2005.
[ BibTeX | 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"
}

A Cavalli, A Mederreg, F Zaidi, P Combes, W Monin, R Castanet, M MacKaya and P Laurencot. Une Plate-forme de Validation Multi-Services et Multi-Protocoles - Résultats d'Expérimentations. Annales des Télécommunications 60(5-6):588–609, June 2005.
[ BibTeX ]

@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"
}

E Bayse, A Cavalli, M Nunez and F Zaidi. A Passive Testing Approach based on Invariants: application to the WAP. In Computer Networks. Volume 48, Elsevier Science, 2005, pages 247-266.
[ BibTeX | pdf ]

@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"
}

A Cavalli, S Maag and F Zaidi. Une approche UML pour la validation des services web. In 5ème Colloque international sur les NOuvelles TEchnologies de la REpartition (NOTERE). September 2005.
[ BibTeX | pdf ]

@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"
}

Delphine Longuet. Une théorie du raffinement orientée propriétés pour les automates communicants. Masters Thesis, Laboratoire de Méthodes Informatiques (LaMI), Université d'Évry-Val d'Essonne, 2005.
[ BibTeX | 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"
}

Marc Aiguier, Pascale Le Gall, Delphine Longuet and Assia Touil. A Temporal Logic for Input Output Symbolic Transition Systems. In 12th Asia-Pacific Software Engineering Conference (APSEC 2005). 2005, 43-50.
[ BibTeX | pdf ]

@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"
}

S -D Gouraud and A Gotlieb. Utilisation des CHRs pour générer des cas de test pour la Machine Virtuelle Java Card. In Journées Francophones de Programmation par Contraintes (JFPC). 2005, 383-392.
[ BibTeX | 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"
}

S -D Gouraud. AuGuSTe: a Tool for Statistical Testing (Experimental results). Number 1400, 2005.
[ BibTeX | pdf ]

@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"
}

S -D Gouraud and A Gotlieb. Using CHRs to Generate Functional Test Cases for the Java Card Virtual Machine. Number 1725, 2005.
[ BibTeX | pdf ]

@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"
}

Achim D Brucker and Burkhart Wolff. Symbolic Test Case Generation for Primitive Recursive Functions. Number 449, Computer Security Group, ETH Zürich, June 2004.
[ BibTeX ]

@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"
}

Nicole Rauch and Burkhart Wolff. Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL. Number 458, ETH Zürich, November 2004.
[ BibTeX | pdf ]

@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 = "old papers",
	title = "Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL",
	year = 2004,
	classification = "unrefereed",
	user = "wolff"
}

A Denise, M -C Gaudel and S -D Gouraud. A Generic Method for Statistical Testing. In IEEE Int. Symp. on Software Reliability Engineering (ISSRE). 2004, 25-34.
[ BibTeX | pdf ]

@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"
}

A Cavalli, S Maag, S Papagiannaki, G Vergiakis and F Zaïdi. A Testing Methodology for an Open Software E-Learning Platform. In 18th IFIP World Computer congress-TC10/WG10.5 Workshop Edutech. August 2004, 165-174.
[ BibTeX ]

@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"
}

A Cavalli, A Mederreg and F Zaïdi. Application of a formal testing methodology to wireless telephony networks. International Journal of the Brazilian Computer Society (JCBS) 10(2):56-68, November 2004. ISSN 0104-6500.
[ BibTeX ]

@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"
}

A Cavalli, A Mederreg, F Zaidi, P Combes, W Monin, R Castanet, M Mackaya and P Laurencot. A Multi-Service and Multi-Protocol Validation Platform Experimentation Results. In R Hierons and R Groz (eds.). Testing of Communicating Systems (Testcom'04). March 2004, 17–19.
[ BibTeX ]

@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"
}

A Denise, M -C Gaudel and S -D Gouraud. A generic method for statistical testing. In 15th. IEEE International Symposium on Software Reliability Engineering (ISSRE). 2004, 25-34.
[ BibTeX | pdf ]

@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"
}

S -D Gouraud. AuGuSTe: un outil pour le Test Statistique. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). 2004, 337-340.
[ BibTeX ]

@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"
}

S -D Gouraud. Utilisation des Structures Combinatoires pour le Test Statistique. Phd Thesis, Université Paris-Sud 11, LRI, 2004.
[ BibTeX | pdf ]

@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"
}

A Denise, M -C Gaudel and S -D Gouraud. A Generic Method For Statistical Testing. Number 1386, 2004.
[ BibTeX ]

@techreport{DeGaGo1386,
	author = "A. Denise and M.-C. Gaudel and S.-D. Gouraud",
	title = "A Generic Method For Statistical Testing",
	year = 2004,
	number = 1386
}

David Basin and Burkhart Wolff (eds.). Theorem Proving in Higher Order Logics, 16th International Conference (TPHOLs 2003). Springer-Verlag, Rome, Italy, September 2003. LNCS 2758..
[ BibTeX ]

@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"
}

Achim D Brucker and Burkhart Wolff. Using Theory Morphisms for Implementing Formal Methods Tools. In Herman Geuvers and Freek Wiedijk (eds.). Types 2002, Proceedings of the workshop Types for Proof and Programs. Series LNCS 2646, Springer-Verlag, 2003.
[ BibTeX ]

@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"
}

Achim D Brucker, Frank Rittinger and Burkhart Wolff. HOL-Z 2.0: A Proof Environment for Z-Specifications. Journal of Universal Computer Science 9(2):152–172, 2003.
[ BibTeX | pdf ]

@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 = "",
	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"
}

Achim D Brucker and Burkhart Wolff. A Case Study of a Formalized Security Architecture. In Thomas Arts and Wan Fokkink (eds.). Eighth International Workshop onFormal Methods for Industrial Critical Systems (FMICS'03) 80. 2003.
[ BibTeX | pdf ]

@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"
}

Nicole Rauch and Burkhart Wolff. Formalizing Java's Two's-Complement Integral Type in Isabelle/HOL. In Electronic Notes in Theoretical Computer Science 80. 2003.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications-softech/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
}

C Besse, A Cavalli and F Zaïdi. Génération de tests d'interopérabilité pour le protocole TCP. In 4ème Colloque Francophone sur la Modélisation des Systèmes Réactifs. October 2003.
[ BibTeX ]

@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"
}

A Cavalli, A Mederreg and F Zaïdi. Application of Formal Testing Methodology to Wireless Telephony Networks. In 2nd International Information and Telecommunications TEchnologies Symposium, I2TS'2003. October 2003.
[ BibTeX ]

@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"
}

A Mederreg, F Zaïdi, P Combes, W Monin, R Castanet, M MacKaya and P Lauren\~cot. Une Plate-forme de Validation Multi-Services et Multi-Protocoles - Résultats d'Expérimentations. In Riguidel Serhouchni M A A. Cavalli (ed.). CFIP'2003 Ingénierie des Protocoles. October 2003, 135–151.
[ BibTeX ]

@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"
}

Fatiha Zaïdi. Platonis - rapport final. Delivrable, Institut National des Télécommunications, France, 2003.
[ BibTeX ]

@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"
}

S -D Gouraud. Génération de Tests à l'Aide d'Outils Combinatoires: Premiers Résultats Expérimentaux. Number 1364, 2003.
[ BibTeX | pdf ]

@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}"
}

Achim D Brucker, Frank Rittinger and Burkhart Wolff. The CVS-Server Case Study: A Formalized Security Architecture. In Dominik Haneberg, Gerhard Schellhorn and Wolfgang Reif (eds.). FM-TOOLS 2002. Series Technical Report, number 2002–11, July 2002, pages 47–52.
[ BibTeX | pdf ]

@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"
}

Achim D Brucker, Frank Rittinger and Burkhart Wolff. A CVS-Server Security Architecture –- Concepts and Formal Analysis. Number 182, Albert-Ludwigs-Universität Freiburg, 2002.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications-softech/papers/2002/cvs_arch.pdf",
	ps = "http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2002/cvs_arch.ps.gz"
}

Achim D Brucker and Burkhart Wolff. HOL-OCL: Experiences, Consequences and Design Choices. In Jean-Marc Jézéquel, Heinrich Hussmann and Stephen Cook (eds.). UML 2002: Model Engineering, Concepts and Tools. Series lncs, number 2460, Springer-Verlag, 2002.
[ BibTeX | pdf ]

@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 = "lncs",
	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
}

Achim D Brucker, Stefan Friedrich, Frank Rittinger and Burkhart Wolff. HOL-Z 2.0: A Proof Environment for Z-Specifications. In Dominik Haneberg, Gerhard Schellhorn and Wolfgang Reif (eds.). FMTOOLS 2002. Series Technical Report, number 2002–11, July 2002, pages 33–38.
[ BibTeX | pdf ]

@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"
}

Achim D Brucker and Burkhart Wolff. A Proposal for a Formal OCL Semantics in Isabelle/HOL. In César Muñoz, Sophiène Tahar and V\'\ictor Carreño (eds.). Theorem Proving in Higher Order Logics. Series lncs, number 2410, Springer-Verlag, 2002, pages 99–114.
[ BibTeX | pdf ]

@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 = "lncs",
	number = 2410,
	pages = "99--114",
	project = "CSFMDOS",
	title = "A Proposal for a Formal {OCL} Semantics in {Isabelle/HOL}",
	year = 2002
}

Burkhart Wolff, Oliver Berthold, Sebastian Clauß, Hannes Federrath, Stefan Köpsell and Andreas Pfitzmann. Towards a Formal Analysis of a Mix Network. Number 171, Albert-Ludwigs-Universität Freiburg, 2002.
[ BibTeX | pdf ]

@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 = "http://www.lri.fr/~wolff/papers/other/tr01.pdf",
	language = "USEnglish",
	classification = "unrefereed"
}

G Lestiennes and M -C Gaudel. Testing processes from formal specifications with inputs, outputs, and datatypes. In IEEE Int. Symp. on Software Reliability Engineering (ISSRE). 2002, 3-14.
[ BibTeX | pdf ]

@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"
}

A Cavalli, A Mederreg and F Zaïdi. Mobiles Services Validation. In Nagib Callaos and al (eds.). The 6th World Conference on Systemics, Cybernics and Informatics. July 2002.
[ BibTeX ]

@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"
}

Cédric Besse, Ana R Cavalli, Myungchul Kim and Fatiha Za\"\idi. Automated Generation of Interoperability Tests. In FIP/TC6/WG6.1 Fourteenth International Conference on Testing of Communicating Systems (Testcom 2002). March 2002, 169-184. ISBN 0-7923-7695-1.
[ BibTeX ]

@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"
}

Fatiha Zaïdi. Mise en place du réseau d'expérimentations. Delivrable PLATONIS-FC-T13/D13, Institut National des Télécommunications, France, 2002.
[ BibTeX ]

@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"
}

Tobias Nipkow, Lawrence C Paulson and Markus Wenzel. Isabelle/HOL –- A Proof Assistant for Higher-Order Logic. Series LNCS, volume 2283, Springer, 2002.
[ BibTeX ]

@book{Nipkow-et-al:2002:tutorial,
	author = "Tobias Nipkow and Lawrence C. Paulson and Markus Wenzel",
	title = "Isabelle/HOL --- A Proof Assistant for Higher-Order Logic",
	series = "LNCS",
	volume = 2283,
	year = 2002,
	publisher = "Springer"
}

Markus Wenzel. Isabelle/Isar –- a versatile environment for human-readable formal proof documents. Phd Thesis, Institut für Informatik, TU München, 2002.
[ BibTeX ]

@phdthesis{Wenzel-PhD,
	author = "Markus Wenzel",
	title = "Isabelle/Isar --- a versatile environment for human-readable formal proof documents",
	school = {Institut f{\"u}r Informatik, TU M{\"u}nchen},
	year = 2002
}

Freek Wiedijk and Markus Wenzel. A comparison of the mathematical proof languages Mizar and Isar.. Journal of Automated Reasoning 29(3-4), 2002.
[ BibTeX ]

@article{Wenzel-Wiedijk:2002,
	author = "Freek Wiedijk and Markus Wenzel",
	title = "A comparison of the mathematical proof languages {Mizar} and {Isar}.",
	journal = "Journal of Automated Reasoning",
	year = 2002,
	volume = 29,
	number = "3-4"
}

Achim D Brucker and Burkhart Wolff. Checking OCL Constraints in Distributed Systems Using J2EE/EJB. Number 157, Albert-Ludwigs-Universität Freiburg, July 2001.
[ BibTeX | pdf ]

@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"
}

Achim D Brucker and Burkhart Wolff. Testing Distributed Component Based Systems Using UML/OCL. In K Bauknecht, W Brauer and Th. Mück (eds.). Informatik 2001 1(157). November 2001, 608–614.
[ BibTeX | pdf ]

@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"
}

Christoph Lüth and Burkhart Wolff. sml_tk: Functional Programming for GUIs – Reference Manual. Number 158, Albert-Ludwigs-Universität Freiburg, July 2001.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications-softech/papers/2001/manual.pdf",
	title = "sml\_tk: Functional Programming for GUIs -- Reference Manual",
	year = 2001
}

Burkhart Wolff. Verifying Explicit Substitution Calculi in Binding Structures with Effect Binding. In Pierre Lescanne (ed.). Workshop on Explicit Substitution Theory and Applications (WESTAPP'01) 210. May 2001, 58 – 71.
[ BibTeX ]

@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 = "workshop",
	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.ethz.ch/WebBIB/publications-softech/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",
	volume = 210,
	year = 2001
}

S -D Gouraud, A Denise, M -C Gaudel and B Marre. A New Way of Automating Statistical Testing Methods. In IEEE International Conference on Automated Software Engineering (ASE). 2001, 5-12.
[ BibTeX | pdf ]

@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"
}

Marie-Claude Gaudel. Testing from Formal Specifications, a Generic Approach. In Dirk Craeynest and Alfred Strohmeier (eds.). Reliable SoftwareTechnologies � Ada-Europe 2001 2043. 2001, 35-48. invited lecture.
[ BibTeX ]

@inproceedings{Ada2001,
	author = "Gaudel, Marie-Claude",
	affiliation = "Universit� de Paris-Sud et CNRS L.R.I B�t. 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
}

A Cavalli, B Defude, Ch. Rinderknecht and F Zaïdi. A Service-Component Testing Method adn Suitable CORBA Architecture. In IEEE Computer Society (ed.). Proceedings of the Sixth IEEE Symposium on Computers and Communications. July 2001, 655–660.
[ BibTeX ]

@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"
}

Fatiha Zaïdi. Contribution a la génération de tests pour les composants de service. Application aux services de Réseau Intelligent. Phd Thesis, Université d'Evry, 2001.
[ BibTeX ]

@phdthesis{Zaidi01,
	author = {Fatiha Za{\"i}di},
	title = "Contribution a la g{\'e}n{\'e}ration de tests pour les composants de service. {A}pplication aux services de {R}{\'e}seau {I}ntelligent",
	year = 2001,
	school = "Universit{\'e} d'Evry"
}

F Zaïdi. Open Problems in protocol testing. Workshop on protocol and dsitributed systems testing, October 2001.
[ BibTeX ]

@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"
}

Fatiha Zaïdi. Test du Service RPVM. Delivrable FC-T222, Institut National des Télécommunications, France, 2001.
[ BibTeX ]

@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"
}

Gertrud Bauer and Markus Wenzel. Calculational reasoning revisited –- an Isabelle/Isar experience. In R J Boulton and P B Jackson (eds.). Theorem Proving in Higher Order Logics (TPHOLs 2001) 2152. 2001.
[ BibTeX ]

@inproceedings{Bauer-Wenzel:2001,
	author = "Gertrud Bauer and Markus Wenzel",
	title = "Calculational reasoning revisited --- an {Isabelle/Isar} experience",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 2001)",
	editor = "R. J. Boulton and P. B. Jackson",
	volume = 2152,
	publisher = "Springer",
	series = "LNCS",
	year = 2001
}

S -D Gouraud. Application de la Génération Aléatoire de Structures Combinatoires au Test de Logiciel. In Approches Formelles dans l'Assistance au Développement de Logiciels (AFADL). 2001, 99-112.
[ BibTeX | pdf ]

@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"
}

S -D Gouraud, A Denise, M -C Gaudel and B Marre. A new way of automating Statistical Testing Methods. In 16th. IEEE International Conference on Automated Software Engineering (ASE). 2001, 5-12.
[ BibTeX | pdf ]

@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"
}

S -D Gouraud, A Denise, M -C Gaudel and B Marre. A New Way of Automating Statistical Testing Methods. Number 1290, 2001.
[ BibTeX ]

@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
}

David Basin, Luca Viganò and Burkhart Wolff. Berichte aus den Instituten: Lehrstuhl für Softwaretechnik und Softwareproduktionsumgebung, Freiburg. PIK (Praxis der Informationsverarbeitung und Kommunikation) 23(4):248–249, 2000.
[ BibTeX | pdf ]

@article{ basin.ea:berichte:2000,
	author = "David Basin and Luca Vigan{\`o} and Burkhart Wolff",
	classification = "conference",
	file = "http://kisogawa.ethz.ch/WebBIB/publications-softech/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.ethz.ch/WebBIB/publications-softech/papers/2000/uebersicht.pdf",
	ps = "http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2000/uebersicht.ps.gz",
	title = {Berichte aus den Instituten: Lehrstuhl f{\"u}r Softwaretechnik und Softwareproduktionsumgebung, Freiburg},
	volume = 23,
	year = 2000
}

Christoph Lüth and Burkhart Wolff. More about TAS and IsaWin: Tools for Formal Program Development. In T Maibaum (ed.). Fundamental Approaches to Software Engineering FASE 2000. Joint European Conferences on Theory and Practice of Software ETAPS 2000 (1783). 2000, 367– 370.
[ BibTeX | pdf ]

@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.ethz.ch/WebBIB/publications-softech/papers/2000/sysdesc.ps.gz",
	pdf = "http://kisogawa.ethz.ch/WebBIB/publications-softech/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."
}

Christoph Lüth and Burkhart Wolff. TAS –- A Generic Window Inference System. In J Harrison and M Aagaard (eds.). Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000 (1869). 2000, 405–422.
[ BibTeX | pdf ]

@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."
}

T Meyer and Burkhart Wolff. Correct Code-Generation in a Generic Framework. In M Aargaard, J Harrison and T Schubert (eds.). TPHOLs 2000: Supplemental Proceedings. July 2000, 213–230.
[ BibTeX | 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://www.lri.fr/~wolff/papers/conf/CodeGen.ps.gz",
	pdf = "http://www.lri.fr/~wolff/papers/conf/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."
}

A Cavalli, B Defude, Ch. Rinderknecht and F Zaïdi. Test de composants de service et exécution de tests sur une plateforme CORBA. In Michel Diaz Patrick Sénac Jean-Pierre Courtiat (ed.). CFIP'2000 Ingénierie des protocoles. October 2000, 363-378.
[ BibTeX ]

@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"
}

F Zaïdi and A Cavalli. Tutorial: Automatic embedded test generation. Université de Reims. International Conference on Software Engineering Applied to Networking and Parallel/Distributed Computing (SNPD'2000), May 2000.
[ BibTeX ]

@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
}

Gertrud Bauer and Markus Wenzel. Computer-Assisted Mathematics at Work –- The Hahn-Banach Theorem in Isabelle/Isar. In Thierry Coquand, Peter Dybjer, Bengt Nordström and Jan Smith (eds.). Types for Proofs and Programs (TYPES 1999) 1956. 2000.
[ BibTeX ]

@inproceedings{Bauer-Wenzel:2000,
	author = "Gertrud Bauer and Markus Wenzel",
	title = "Computer-Assisted Mathematics at Work --- The {Hahn-Banach Theorem} in {Isabelle/Isar}",
	booktitle = "Types for Proofs and Programs (TYPES 1999)",
	editor = {Thierry Coquand and Peter Dybjer and Bengt Nordstr{\"o}m and Jan Smith},
	volume = 1956,
	publisher = "",
	series = "",
	year = 2000
}

Christoph Lüth and Burkhart Wolff. Functional Design and Implementation of Graphical User Interfaces for Theorem Provers. Journal of Functional Programming 9(2):167– 189, 1999.
[ BibTeX | pdf ]

@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 = "",
	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.ethz.ch/WebBIB/publications-softech/papers/1999/fungui.ps.gz",
	language = "USenglish",
	pdf = "http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/1999/fungui.pdf"
}

P R James, M Endler and M -C Gaudel. Development of an Atomic Broadcast Protocol using LOTOS. Software Practice and Experience 29(8):699-719, 1999.
[ BibTeX ]

@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"
}

A Cavalli, D Lee, C Rinderknecht and F Zaïdi. Hit-or-Jump: An algorithm for Embedded Testing with Applications to In Services. In Jianping Wu and al. (eds.). Proceeding of IFIP International conference FORTE/PSTV'99. October 1999, 41-56.
[ BibTeX ]

@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"
}

Ana Cavalli, David Lee, Christian Rinderknecht and Fatiha Zaïdi. Un algorithme pour le test imbriqué avec des applications aux services R.I. In Actes de la 3ème édition des journées Doctorales Informatique et Réseaux. November 1999, 22-24.
[ BibTeX ]

@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"
}

Stefan Berghofer and Markus Wenzel. Inductive datatypes in HOL –- lessons learned in Formal-Logic Engineering. In Y Bertot, G Dowek, A Hirschowitz, C Paulin and L Thery (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1999) 1690. 1999.
[ BibTeX ]

@inproceedings{Berghofer-Wenzel:1999,
	author = "Stefan Berghofer and Markus Wenzel",
	title = "Inductive datatypes in {HOL} --- lessons learned in {Formal-Logic Engineering}",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 1999)",
	editor = "Bertot, Y. and Dowek, G. and Hirschowitz, A. and Paulin, C. and Thery, L.",
	volume = 1690,
	publisher = "Springer",
	series = "LNCS",
	year = 1999
}

Florian Kammüller, Markus Wenzel and Lawrence C Paulson. Locales: A Sectioning Concept for Isabelle. In Y Bertot, G Dowek, A Hirschowitz, C Paulin and L Thery (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1999) 1690. 1999.
[ BibTeX ]

@inproceedings{Kamm-et-al:1999,
	author = {Florian Kamm{\"u}ller and Markus Wenzel and Lawrence C. Paulson},
	title = "Locales: A Sectioning Concept for {Isabelle}",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 1999)",
	editor = "Bertot, Y. and Dowek, G. and Hirschowitz, A. and Paulin, C. and Thery, L.",
	volume = 1690,
	publisher = "Springer",
	series = "LNCS",
	year = 1999
}

Markus Wenzel. Isar –- a Generic Interpretative Approach to Readable Formal Proof Documents. In Y Bertot, G Dowek, A Hirschowitz, C Paulin and L Thery (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1999) 1690. 1999.
[ BibTeX ]

@inproceedings{Wenzel:1999,
	author = "Markus Wenzel",
	title = "{Isar} --- a Generic Interpretative Approach to Readable Formal Proof Documents",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 1999)",
	editor = "Bertot, Y. and Dowek, G. and Hirschowitz, A. and Paulin, C. and Thery, L.",
	volume = 1690,
	publisher = "Springer",
	series = "LNCS",
	year = 1999
}

Chritoph Lüth, Einar W Karlsen, Kolyang, Stefan Westmeier and Burkhart Wolff. HOL-Z in the UniForM-Workbench – a Case Study in Tool Integration for Z. In J Bowen (ed.). 11. International Conference of Z Users ZUM'98. 1998, 116–134.
[ BibTeX ]

@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.ethz.ch/WebBIB/publications-softech/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."
}

C Lüth, E W Karlsen, Kolyang, S Westmeier and B Wolff. Tool integration in the UniForM Workbench. In Berghammer and Hoffmann (eds.). Workshop on Tool Support for System Specification, Development, and Verification. 1998.
[ BibTeX ]

@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 = "http://www.lri.fr/~wolff/papers/conf/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"
}

Haykal Tej, Christoph Lüth and Burkhart Wolff. Generic Transformational Program Development.. Unpublished Paper., 1998
[ BibTeX | pdf ]

@unpublished{LTW98,
	author = {Haykal Tej and Christoph L\"uth and Burkhart Wolff},
	title = "Generic Transformational Program Development.",
	note = "Unpublished Paper.",
	pdf = "http://www.lri.fr/~wolff/papers/conf/gentraf.pdf",
	year = 1998,
	classification = "unrefereed"
}

M -C Gaudel and P R James. Testing Algebraic Data Types and Processes: a unifying theory. Formal Aspects of Computing 10(5-6):436–451, 1998.
[ BibTeX | pdf ]

@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"
}

Wolfgang Naraschewski and Markus Wenzel. Object-Oriented Verification based on Record Subtyping in Higher-Order Logic. In Jim Grundy and Malcom Newey (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1998) 1479. 1998.
[ BibTeX ]

@inproceedings{Naraschewski-Wenzel:1998,
	author = "Wolfgang Naraschewski and Markus Wenzel",
	title = "Object-Oriented Verification based on Record Subtyping in {Higher-Order Logic}",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 1998)",
	editor = "Jim Grundy and Malcom Newey",
	publisher = "Springer",
	series = "LNCS",
	volume = 1479,
	year = 1998
}

Kolyang, C Lüth, T Meier and B Wolff. TAS and IsaWin: Generic Interfaces for Transformational Program Development and Theorem Proving. In Dauchet M M. Bidoit (ed.). TAPSOFT 97: Theory and Practice of Software Development. 1997, 855–858.
[ BibTeX ]

@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"
}

Kolyang, C L\"uth, T Meier and B Wolff. Generic Interfaces for Transformation Systems and Interactive Theorem Provers.. In Buth B K.Berghammer J.Peleska (ed.). Proceedings of the “International Workshop for Tool Support in Verification and Validation{\'}{\'}. 1997.
[ BibTeX ]

@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"
}

H Tej and B Wolff. A Corrected Failure-Divergence Model for CSP in Isabelle/HOL. In J Fitzgerald, C B Jones and P Lucas (eds.). Proceedings of the FME 97 –- Industrial Applications and Strengthened Foundations of Formal Methods. 1997, 318–337.
[ BibTeX | pdf ]

@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 = "http://www.lri.fr/~wolff/papers/conf/CSP.ps.gz",
	pdf = "http://www.lri.fr/~wolff/papers/conf/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"
}

B Wolff. A Generic Calculus of Transformations. Phd Thesis, Universität Bremen, Aachen, 1997.
[ BibTeX ]

@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 = "http://www.lri.fr/~wolff/papers/other/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"
}

M Wenzel. Type Classes and Overloading in Higher-Order Logic. In Elsa L Gunter and Amy Felty (eds.). Theorem Proving in Higher Order Logics (TPHOLs 1997) 1275. 1997.
[ BibTeX ]

@inproceedings{Wenzel:1997,
	author = "M. Wenzel",
	title = "Type Classes and Overloading in Higher-Order Logic",
	booktitle = "Theorem Proving in Higher Order Logics (TPHOLs 1997)",
	editor = "Elsa L. Gunter and Amy Felty",
	volume = 1275,
	publisher = "Springer",
	series = "LNCS",
	year = 1997
}

Kolyang, C Lüth, T Meier and B Wolff. Generating Graphical User-Interfaces in a Functional Setting. In N Merriam (ed.). Proceedings of the User Interfaces for Theorem Provers (UITP 96). 1996.
[ BibTeX ]

@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"
}

Kolyang, T Santen and B Wolff. Correct and User-Friendly Implementation of Transformation Systems. In M -C Gaudel and J Woodcock (eds.). FME 96 –- Industrial Benefits and Advances in Formal Methods. 1996, 629–648.
[ BibTeX | pdf ]

@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 = "http://www.lri.fr/~wolff/papers/conf/yats.ps.gz",
	pdf = "http://www.lri.fr/~wolff/papers/conf/yats.pdf",
	language = "USEnglish",
	doi = "10.1007/3-540-60973-3_111",
	classification = "conference"
}

Kolyang, T Santen and B Wolff. A Structure Preserving Encoding of Z in Isabelle/HOL. In J Wright, J Grundy and J Harrison (eds.). Theorem Proving in Higher Order Logics –- 9th International Conference. 1996, 283–298.
[ BibTeX | pdf ]

@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 = "http://www.lri.fr/~wolff/papers/conf/SPEZ_HOL.R.23.ps.gz",
	pdf = "http://www.lri.fr/~wolff/papers/conf/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"
}

C Lüth, S Westmeier and B Wolff. sml_tk: Functional Programming for Graphical User Interfaces. Number 8/96, Universität Bremen, 1996.
[ BibTeX ]

@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"
}

M -C Gaudel, P Dauchy and C Khoury. A Formal Specification of the Steam-Boiler Control Problem by Algebraic Specifications with Implicit State. In Formal Methods for Industrial Applications: specifying and programming the Steam Boiler Control. Series Lecture Notes in Computer Science, volume 1165, Springer-Verlag, 1996, pages 233-264.
[ BibTeX | pdf ]

@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"
}

B Krieg-Brückner, J Liu, H Shi and B Wolff. Towards Correct, Efficient and Re-usable Transformational Developments. In M Broy and S Jähnichen (eds.). KORSO –- Methods, Languages, and Tools for the Construction of Correct Software. 1995, 270–284.
[ BibTeX ]

@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"
}

Kolyang and B Wolff. Development by Refinement Revisited: Lessons learnt from an example.. In G Snelting (ed.). Beiträge der GI-Fachtagung “Softwaretechnik 95{\'}{\'}, Braunschweig. 1995, 57–66.
[ BibTeX ]

@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"
}

M -C Gaudel. Testing can be formal, too. In TAPSOFT'95, International Joint Conference, Theory And Practice of Software Development 915. 1995, 82-96.
[ BibTeX | pdf ]

@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"
}

A Arnold, M Gaudel and B Marre. An Experiment on the Validation of a Specification by Heterogeneous Formal Means: The Transit Node. In 5th IFIP Working Conference on Dependable Computing for Critical Applications (DCCA5). 1995, 24–34.
[ BibTeX ]

@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"
}

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

@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"
}

G Bernot, M -C Gaudel and B Marre. A Formal Approach to Software Testing. In 2nd International Conference on Algebraic Methodology and Software Technology (AMAST) (670). 1992, 243-253.
[ BibTeX | pdf ]

@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"
}

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

@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"
}

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

@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"
}