wolff.bib

@preamble{{\def{\ac}[1]{\textsc{#1}} } # {\def{\acs}[1]{\textsc{#1}} } # {\def{\acf}[1]{\textsc{#1}} } # {\def{\TAP}{T\kern-.1em\lower-.5ex\hbox{A}\kern-.1em P} } # {\def{\leanTAP}{\mbox{\sf lean\it\TAP}} } # {\def{\holz}{\textsc{hol-z}} } # {\def{\holocl}{\textsc{hol-ocl}} } # {\def{\holboogie}{\textsc{hol}-Boogie} } # {\def{\isbn}{\textsc{isbn}} } # {\def{\doi}[1]{\href{http://dx.doi.org/#1}{doi: {\urlstyle{rm}\nolinkurl{#1}}}}} # {\def{\unixcmd}[1]{\textsc{#1}} } # {\def{\UML}{\textsc{uml}} } # {\def{\OCL}{\textsc{ocl}} } # {\def{\HOL}{\textsc{hol}} } # {\def{\IMPOO}{\textsc{imp++}} } # {\def{\posix}{\textsc{posix}} } # {\def{\testgen}{\textsc{HOL-TestGen}} } # {\def{\testgenFW}{\textsc{TestGenFW}} } # {\def{\item}{} }}
@inproceedings{AissatVW2016,
  title = {Infeasible Paths Elimination by Symbolic Execution Techniques: 
              Proof of Correctness and Preservation of Paths},
  author = {Aissat, R. and Voisin, F. and Wolff, B.},
  booktitle = {{ITP'16}},
  abstract = {TRACER is a tool for verifying safety properties of sequential C 
              programs. TRACER attempts at building a finite symbolic execution 
              graph which over-approximates the set of all concrete reachable 
              states and the set of feasible paths.
              
              We present an abstract framework for TRACER and similar CEGAR-like 
              systems. The framework provides 1) a graph-transformation based 
              method for reducing the feasible paths in control-flow graphs, 2) 
              a model for symbolic execution, subsumption, predicate abstraction 
              and invariant generation. 
              
              In this framework we formally prove two key properties: correct 
              construction of the symbolic states and preservation of feasible 
              paths. The framework focuses on core operations, leaving to 
              concrete prototypes to “fit in” heuristics for combining them.},
  year = {2016},
  series = {Lecture Notes in Computer Science},
  volume = {9762},
  pdf = {https://www.lri.fr/~wolff/papers/conf/2016-itp-InfPathsNSE.pdf},
  location = {Vienna}
}
@inproceedings{DBLP:conf/tap/BruckerW16,
  author = {Achim D. Brucker and
               Burkhart Wolff},
  title = {Monadic Sequence Testing and Explicit Test-Refinements},
  booktitle = {Tests and Proofs - 10th International Conference, {TAP} 2016, Held
               as Part of {STAF} 2016, Vienna, Austria, July 5-7, 2016, Proceedings},
  volume = {LNCS 7942},
  series = {Lecture Notes in Computer Science},
  pages = {17--36},
  year = {2016},
  abstract = {Abstract We present an abstract framework for sequence testing 
               that is implemented in Isabelle/HOL-TestGen. Our framework is 
               based on the theory of state-exception monads, explicitly modelled 
               in HOL, and can cope with typed input and output, interleaving 
               executions including abort, and synchronisation.
               
               The framework is particularly geared towards symbolic execution 
               and has proven effective in several large case-studies involving 
               system models based on large (or infinite) state.
               
               On this basis, we rephrase the concept of test-refinements for 
               inclusion, deadlock and IOCO-like tests, together with a formal 
               theory of its rela- tion to traditional, IO-automata based notions.},
  url = {http://dx.doi.org/10.1007/978-3-319-41135-4_2},
  pdf = {https://www.brucker.ch/bibliography/download/2016/brucker.ea-monadic-sequence-testing-2016.pdf},
  doi = {10.1007/978-3-319-41135-4_2}
}
@techreport{AGVW2016,
  author = {Aissat, R. and Gaudel, M.-C. and Voisin, F. and Wolff, B.},
  title = {Pruning Infeasible Paths via Graph Transformations and
               Symbolic Execution: a Method and a Tool},
  number = {1588},
  institution = {L.R.I., Univ. Paris-Sud},
  url = {https://www.lri.fr/srubrique.php?news=33},
  year = {2016}
}
@techreport{brucker.ea:hol-testgen:2016,
  author = {Achim D. Brucker and Lukas Br{\"u}gger and Abderrahmane
		       Feliachi and Chantal Keller and Matthias P. Krieger and
		       Delphine Longuet and Yakoub Nemouchi and Fr{\'e}d{\'e}ric
		       Tuong and Burkhart Wolff },
  institution = {Laboratoire en Recherche en Informatique (LRI),
		         Universit\'e Paris-Sud 11, France},
  language = {USenglish},
  month = apr,
  title = {{HOL-TestGen} 1.8.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 = {2016},
  number = {1586},
  num_pages = {111},
  pdf = {https://www.brucker.ch/bibliography/download/2016/brucker.ea-hol-testgen-2016.pdf},
  public = {yes},
  url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2016}
}
@techreport{brucker.ea:formal-semantics-ocl-2.5:2015,
  author = {Achim D. Brucker and Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
  institution = {LRI, Univ Paris Sud, CNRS, Centrale Sup\'elec,
		           Universit\'e Paris-Saclay, France},
  language = {USenglish},
  month = sep,
  title = {Featherweight {OCL}: {A} {P}roposal for a {M}achine-{C}hecked {F}ormal
		  {S}emantics for {OCL} 2.5},
  categories = {holocl},
  classification = {unrefereed},
  areas = {formal methods, software},
  year = {2015},
  number = {1582},
  num_pages = {196},
  public = {yes},
  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 a textual annotation language, originally 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. Many of these
		  corner cases had been subject to formal analysis since more
		  than ten years.
		  
		  The situation complicated with the arrival of version 2.3
		  of the OCL standard. OCL was aligned with the latest
		  version of UML: this led to the extension of the
		  three-valued logic by a second exception element, called
		  null. While the first exception element invalid has a
		  strict semantics, null has a non strict interpretation. The
		  combination of these semantic features lead to remarkable
		  confusion for implementors of OCL compilers and
		  interpreters.
		  
		  In this paper, we provide a formalization of the core of
		  OCL in HOL. It provides 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. Moreover, we describe a coding-scheme for UML
		  class models that were annotated by code-invariants and
		  code contracts. An implementation of this coding-scheme has
		  been undertaken: it consists of a kind of compiler that
		  takes a UML class model and translates it into a family of
		  definitions and derived theorems over them capturing the
		  properties of constructors and selectors, tests and casts
		  resulting from the class model. However, this compiler is
		  not included in this document.
		  
		  Our formalization reveals several inconsistencies and
		  contradictions in the current version of the OCL standard.
		  They reflect a challenge to define and implement OCL tools
		  in a uniform manner. Overall, this document is intended to
		  provide the basis for a machine-checked text ``Annex A'' of
		  the OCL standard targeting at tool implementors. },
  pdf = {https://www.lri.fr/~bibli/Rapports-internes/2015/RR1582.pdf},
  url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-formal-semantics-ocl-2.5-2015}
}
@article{tuong.ea:meta-model:2015,
  author = {Fr{\'e}d{\'e}ric Tuong and Burkhart Wolff},
  title = {A {M}eta-{M}odel for the {I}sabelle {API}},
  journal = {Archive of Formal Proofs},
  year = {2015},
  url = {https://www.brucker.ch/bibliography/abstract/tuong.ea-meta-model-2015},
  issn = {2150-914x},
  categories = {holocl},
  public = yes
}
@inbook{used-fm:2015,
  author = {Yakoub Nemouchi and Abderrahmane Feliachi and 
          Burkhart Wolff and Cyril Proch},
  year = 2015,
  chapter = {Using Isabelle/HOL in Certification Processes: 
           A System Description and Mandatory Recommendations},
  editor = {Sergey Tverdyshev and  Oto Havle and Holger Blasum and Bruno Langenstein
           and Werner Stephan and Abderrahmane Feliachi and Yakoub Nemouchi and
           Burkhart Wolff and  Cyril Proch and Freek Verbeek and Julien Schmaltz},
  title = {Used Formal Methods},
  publisher = {The EURO-MILS Project},
  note = {available from the Project site: \url{http://www.euromils.eu/downloads/Deliverables/Y2/2015-EM-UsedFormalMethods-WhitePaper-October2015.pdf}},
  doi = {http://dx.doi.org/10.5281/zenodo.47297}
}
@article{feliachi-wolff:SymbTestgenCirta:2013,
  author = {Abderrahmane Feliachi and  Marie-Claude Gaudel and Burkhart Wolff},
  title = {Symbolic Test-generation in {HOL}-{T}est{G}en/{C}irTA: A Case Study},
  journal = {Int. J. Software Informatics},
  volume = {9},
  number = {2},
  year = {2015},
  pages = {177--203},
  abstract = {HOL-TestGen/CirTA is a theorem-prover based test generation 
                  environment for specifications written in Circus, a 
                  process-algebraic specification language in the tradition 
                  of CSP. HOL-TestGen/CirTA is based on a formal embedding of 
                  its semantics in Isabelle/HOL, allowing to derive rules over 
                  specification constructs in a logically safe way. 
                  Beyond the derivation of algebraic laws and calculi for 
                  process refinement, the originality of HOL-TestGen/ CirTA 
                  consists in an entire derived theory for the generation of 
                  symbolic test-traces, including optimized rules for test-generation 
                  as well as rules for symbolic execution. The deduction process 
                  is automated by Isabelle tactics, allowing to protract the 
                  state-space explosion resulting from blind enumeration of data.
                  
                  The implementation of test-generation procedures in CirTA is 
                  completed by an integrated tool chain that transforms the 
                  initial Circus specification of a system into a set of 
                  equivalence classes (or “symbolic tests”), which were compiled 
                  to conventional JUnit test-drivers.
                  
                  This paper describes the novel tool-chain based on prior 
                  theoretical work on semantics and test-theory and attempts 
                  an evaluation via a medium-sized case study performed on a 
                  component of a real-world safety-critical medical monitoring 
                  system written in Java. We provide experimental measurements 
                  of the kill-capacity of implementation mutants.},
  public = yes,
  url = {https://www.lri.fr/~wolff/papers/journals/2015-cirta-case-study.pdf}
}
@article{brucker-wolff:FormalFirewallTest:2013,
  author = {Achim D. Brucker and Lukas Br\"ugger and Burkhart Wolff},
  title = {Formal Firewall Conformance 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}
}
@inproceedings{DBLP:conf/models/VanBBTVWY15,
  author = {Hai Nguyen Van and
               Thibaut Balabonski and
               Fr{\'{e}}d{\'{e}}ric Boulanger and
               Safouan Taha and
               Beno{\^{\i}}t Valiron and
               Burkhart Wolff and
               Lina Ye},
  title = {Towards a Formal Semantics of the {TESL} Specification Language},
  booktitle = {Joint Proceedings of the 3rd International Workshop on the Globalization
               Of Modeling Languages and the 9th International Workshop on Multi-Paradigm
               Modeling co-located with {ACM/IEEE} 18th International Conference
               on Model Driven Engineering Languages and Systems, GEMOC+MPM@MoDELS
               2015, Ottawa, Canada, September 28, 2015.},
  pages = {14--19},
  year = {2015},
  url = {http://ceur-ws.org/Vol-1511/paper-03.pdf},
  timestamp = {Fri, 20 Nov 2015 15:31:33 +0100},
  biburl = {http://dblp.uni-trier.de/rec/bib/conf/models/VanBBTVWY15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@incollection{brucker.ea:ipc-testing:2015,
  abstract = {In this paper, we adapt model-based testing techniques to
		  concurrent code, namely for test generations of an
		  (industrial) OS kernel called PikeOS\@. Since our
		  data-models are complex, the problem is out of reach of
		  conventional model-checking techniques. Our solution is
		  based on symbolic execution implemented inside the
		  interactive theorem proving environment Isabelle/HOL
		  extended by a plugin with test generation facilities called
		  HOL-TestGen.
		  
		  As a foundation for our symbolic computing techniques, we
		  refine the theory of monads to embed interleaving
		  executions with abort, synchronization, and shared memory
		  to a general but still optimized behavioral test framework.
		  
		  This framework is instantiated by a model of PikeOS
		  inter-process communication system-calls. Inheriting a
		  micro-architecture going back to the L4 kernel, the system
		  calls of the IPC-API are internally structured by atomic
		  actions; according to a security model, these actions can
		  fail and must produce error-codes. Thus, our tests reveal
		  errors in the enforcement of the security model.},
  keywords = {test program generation, symbolic test case generations,
		  black box testing, testing operating systems,
		  certification, CC, concurrency, interleaving},
  location = {San Francisco, California, USA},
  author = {Achim D. Brucker and Oto Havle and Yakoub Nemouchi and
		  Burkhart Wolff},
  title = {Testing the IPC Protocol for a Real-Time Operating
		  System},
  booktitle = {Working Conference on Verified Software: Theories, Tools,
		  and Experiments},
  language = {USenglish},
  publisher = {Springer-Verlag},
  address = {Heidelberg},
  series = {Lecture Notes in Computer Science},
  number = {9593},
  isbn = {3-540-14031-X},
  editor = {Arie Gurfinkel and Sanjit A. Seshia},
  pdf = {http://www.lri.fr/~wolff/papers/conf/2015-vstte-ipc-testing.pdf},
  issn = {0302-9743},
  categories = {holtestgen},
  classification = {conference},
  areas = {formal methods},
  year = {2015},
  public = {yes},
  doi = {10.1007/978-3-319-29613-5_3},
  url = {https://www.brucker.ch/bibliography/abstract/brucker.ea-ipc-testing-2015}
}
@inproceedings{DBLP:conf/nfm/VerbeekHSTBL0WN15,
  author = {Freek Verbeek and
               Oto Havle and
               Julien Schmaltz and
               Sergey Tverdyshev and
               Holger Blasum and
               Bruno Langenstein and
               Werner Stephan and
               Burkhart Wolff and
               Yakoub Nemouchi},
  title = {Formal {API} Specification of the PikeOS Separation Kernel},
  booktitle = {{NASA} Formal Methods - 7th International Symposium, {NFM} 2015, Pasadena,
               CA, USA, April 27-29, 2015, Proceedings},
  pages = {375--389},
  year = {2015},
  url = {http://dx.doi.org/10.1007/978-3-319-17524-9_26},
  doi = {10.1007/978-3-319-17524-9_26},
  timestamp = {Wed, 08 Apr 2015 14:02:16 +0200},
  biburl = {http://dblp.uni-trier.de/rec/bib/conf/nfm/VerbeekHSTBL0WN15},
  bibsource = {dblp computer science bibliography, http://dblp.org}
}
@inproceedings{DBLP:conf/models/LonguetTW14,
  author = {Delphine Longuet and Fr{\'{e}}d{\'{e}}ric Tuong and Burkhart Wolff},
  title = {Towards a {T}ool for {F}eatherweight {OCL:} {A} {C}ase {S}tudy {O}n {S}emantic
               {R}eflection},
  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}
}
@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}
}
@article{UPF-AFP,
  author = {Achim D. Brucker and Lukas Br{\"u}gger and Burkhart Wolff},
  title = {The {U}nified {P}olicy {F}ramework {(UPF)}},
  journal = {Archive of Formal Proofs},
  month = nov,
  year = 2014,
  note = {\url{http://afp.sf.net/entries/UPF.shtml},
            Formal proof development},
  issn = {2150-914x}
}
@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 = jul,
  year = 2014,
  note = {\url{http://afp.sf.net/entries/CISC-Kernel.shtml},
            Formal proof development},
  issn = {2150-914x}
}
@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}
}
@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}
}
@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}
}
@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.}
}
@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-tap-tproc-testgen.pdf},
  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}
}
@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}
}
@article{Feliachi-Wolff-Gaudel-AFP12,
  author = {Abderrahmane Feliachi and Burkhart Wolff and Marie-Claude Gaudel},
  title = {Isabelle/Circus},
  journal = {Archive of Formal Proofs},
  month = jun,
  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}
}
@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}
}
@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 = apr,
  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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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.}
}
@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}
}
@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.}
}
@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.}
}
@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}
}
@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},
  year = {2013}
}
@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 = sept,
  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}
}
@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}
}
@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}
}
@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}
}
@incollection{brucker.ea:hol-testgen:2009,
  title = {{HOL-TestGen:} {A}n {I}nteractive {T}est-case {G}eneration {F}ramework},
  abstract = {We present HOL-TestGen, an extensible test environment for
		  specification-based testing build upon the proof assistant
		  Isabelle. HOL-TestGen leverages the semi-automated
		  generation of test theorems (a form of a partition), and
		  their refinement to concrete test data, as well as the
		  automatic generation of a test driver for the execution and
		  test result verification.
		  
		  HOL-TestGen can also be understood as a unifying technical
		  and conceptual framework for presenting and investigating
		  the variety of unit and sequence test techniques in a
		  logically consistent way. },
  keywords = {symbolic test case generations, black box testing, white
		  box testing, theorem proving, interactive testing},
  location = {York, UK},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Fundamental Approaches to Software Engineering
		  {(FASE09)}},
  language = {USenglish},
  publisher = {Springer-Verlag},
  address = {Heidelberg},
  series = {Lecture Notes in Computer Science},
  number = {5503},
  doi = {10.1007/978-3-642-00593-0_28},
  pages = {417--420},
  editor = {Marsha Chechik and Martin Wirsing},
  categories = {holtestgen},
  classification = {conference},
  year = {2009},
  pdf = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2009/brucker.ea-hol-testgen-2009.ps.gz},
  public = {yes},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-testgen-2009}
}
@incollection{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}
}
@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
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@incollection{brucker.ea:cvs-server:2002,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002},
  author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  title = {The {CVS}-Server Case Study: A Formalized Security
		  Architecture},
  editor = {Dominik Haneberg and Gerhard Schellhorn and Wolfgang
		  Reif},
  booktitle = {FM-TOOLS 2002},
  classification = {conference},
  year = 2002,
  series = {Technical Report},
  number = {2002--11},
  pages = {47--52},
  month = jul,
  organization = {University Augsburg},
  address = {Augsburg},
  pdf = {http://www.brucker.ch/bibliography/download/2002/fmtools_cvs_02.pdf},
  language = {USenglish},
  abstract = {CVS is a widely known version management system.
		  Configured in server mode, it can be used for the
		  distributed development of software as well as its
		  distribution from a central database called the
		  \emph{repository}. In this setting, a number of security
		  mechanisms have to be integrated into the CVS-server
		  architecture.
		  
		  We present an abstract formal model of the access control
		  aspects of a CVS-server architecture enforcing a role-based
		  access control on the data in the repository. This abstract
		  architecture is refined to an implementation architecture,
		  which represents (an abstraction of) a concrete CVS-server
		  configuration running in a POSIX/UNIX environment.
		  
		  Both the abstract as well as the concrete architecture are
		  specified in the language Z. The specification is compiled
		  to HOL-Z, such that refinement proofs for this case study
		  can be done in Isabelle/HOL. },
  project = {FSA}
}
@techreport{brucker.ea:cvs-server:2002-b,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-cvs-server-2002-b},
  author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  institution = {Albert-Ludwigs-Universit{\"a}t Freiburg},
  language = {USenglish},
  number = 182,
  title = {A {CVS-Server} Security Architecture --- Concepts and
		  Formal Analysis},
  abstract = {We present a secure architecture of a CVS-server, its
		  implementation (i.e. mainly its configuration) and its
		  formal analysis. Our CVS-server is uses cvsauth, that
		  provides protection of passwords and protection of some
		  internal data of the CVS repository. In contrast to other
		  (security oriented) CVS-architectures, our approach allows
		  the CVS-server run on an open filesystem, i.e. a filesystem
		  where users can have direct access both by CVS-commands and
		  by standard UNIX/POSIX commands such as \unixcmd{mv}.
		  
		  For our secure architecture of the CVS-server, we provide a
		  formal specification and security analysys. The latter is
		  based on a refinement mapping high-level security
		  requirements on the architecture on low-level security
		  mechanisms on the UNIX/POSIX filesystem level.
		  
		  The purpose of the formal analysis of the secure CVS-server
		  architecture is twofold: First, it is the bases for the
		  specification of mutual security properties such as
		  non-repudiation, authentication and access control for this
		  architecture. Second, the mapping of the architecture on
		  standard security implementation technology is described.
		  
		  Thus, our approach can be seen as a method to give a formal
		  underpinning for the usually tricky business of system
		  administrators.},
  keywords = {security architecture, Concurrent Versions System (CVS),
		  Z, formal methods, refinement},
  year = 2002,
  classification = {unrefereed},
  num_pages = 100,
  pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2002/cvs_arch.pdf},
  ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/2002/cvs_arch.ps.gz}
}
@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 = {https://www.lri.fr/~wolff/papers/journals/brucker.ea-extensible-2008-b},
  title = {{A}n {E}xtensible {E}ncoding of {O}bject-oriented {D}ata {M}odels in {HOL} with an {A}pplication to {IMP++}},
  volume = {Selected Papers of the AVOCS-VERIFY Workshop 2006},
  doi = {10.1007/s10817-008-9108-3},
  pages = {219-249},
  volume = 41,
  number = {3--4},
  year = 2008
}
@incollection{brucker.ea:extensible:2008-b,
  abstract = {We present a datatype package that enables the shallow
		  embedding technique to object-oriented specification and
		  programming languages. This datatype package incrementally
		  compiles an object-oriented data model to a theory
		  containing object-universes, constructors, accessors
		  functions, coercions between dynamic and static types,
		  characteristic sets, their relations reflecting
		  inheritance, and the necessary class invariants. The
		  package is conservative, i.e., all properties are derived
		  entirely from axiomatic definitions. As an application, we
		  use the package for an object-oriented core-language called
		  imp++, for which correctness of a Hoare-Logic with respect
		  to an operational semantics is proven. },
  address = {Paphos, Cyprus},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Proceedings of the European Conference of Object-Oriented
		  Programming (ECOOP 2008)},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/978-3-540-70592-5_19},
  editor = {Jan Vitek},
  isbn = {0302-9743},
  language = {USenglish},
  classification = {conference},
  month = {July},
  pages = {438--462},
  pdf = {http://kisogawa.ethz.ch/WebBIB/publications/papers/2008/brucker.ea-datatype-2008.pdf},
  publisher = {Springer-Verlag},
  series = {LNCS 5142},
  title = {Extensible Universes for Object-Oriented Data Models },
  url = {http://www.springerlink.com/content/416483625116hw37/?p=b2e4cfb4996441a9b171c4594f015499&pi=18},
  year = 2008,
  user = {lukasbru}
}
@inproceedings{brucker.ea:formal:2008,
  title = {{A} {F}ormal {P}roof {E}nvironment for {UML/OCL}},
  abstract = {We present the theorem proving environment HOL-OCL that is
		  integrated in a MDE framework. HOL-OCL allows to reason
		  over UML class models annotated with OCL
		  specifications. Thus, HOL-OCL strengthens a crucial part of
		  the UML to an object-oriented formal method. \holocl
		  provides several derived proof calculi that allow for
		  formal derivations establishing the validity of UML/OCL
		  formulae. These formulae arise naturally when checking the
		  consistency of class models, when formally refining
		  abstract models to more concrete ones or when discharging
		  side-conditions from model-transformations.},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {Proceedings of Formal Aspects of Software Engineering
		  (FASE 2008)},
  isbn = {0302-9743},
  language = {USenglish},
  classification = {conference},
  pages = {97--101},
  doi = {10.1007/978-3-540-78743-3_8},
  pdf = {http://kisogawa.inf.ethz.ch/WebBIB/publications/papers/2008/2008-fase-hol-ocl.pdf},
  publisher = {Springer Berlin / Heidelberg},
  series = {Lecture Notes in Computer Science},
  volume = 4961,
  year = 2008
}
@techreport{brucker.ea:hol-ocl-book:2006,
  author = {Achim D. Brucker and Burkhart Wolff},
  institution = {ETH Z{\"u}rich},
  language = {USenglish},
  title = {The {HOL-OCL} {B}ook},
  classification = {unrefereed},
  categories = {holocl},
  year = 2006,
  number = 525,
  pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-hol-ocl-book-2006.pdf},
  abstract = {HOL-OCL is an interactive proof environment for the Object
		  Constraint Language (OCL). It is implemented as a shallow
		  embedding of OCL into the Higher-order Logic (HOL) instance
		  of the interactive theorem prover Isabelle. HOL-OCL defines
		  a machine-checked formalization of the semantics as
		  described in the standard for OCL 2.0. This conservative,
		  shallow embedding of UML/OCL into Isabelle/HOL includes
		  support for typed, extensible UML data models supporting
		  inheritance and subtyping inside the typed lambda-calculus
		  with parametric polymorphism. As a consequence of
		  conservativity with respect to higher-order logic (HOL), we
		  can guarantee the consistency of the semantic model.
		  Moreover, HOL-OCL provides several derived calculi for
		  UML/OCL that allow for formal derivations establishing the
		  validity of UML/OCL formulae. Elementary automated support
		  for such proofs is also provided top },
  bibkey = {brucker.ea:hol-ocl-book:2006},
  keywords = {security, SecureUML, UML, OCL, HOL-OCL,
		  model-transformation}
}
@incollection{brucker.ea:hol-ocl:2002,
  title = {{HOL-OCL}: Experiences, Consequences and Design Choices},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-hol-ocl-2002},
  abstract = {Based on experiences gained from an embedding of the
		  Object Constraint Language (OCL) in higher-order
		  logic~\cite{brucker.ea:proposal:2002}, we explore several
		  key issues of the design of a formal semantics of the OCL.
		  These issues comprise the question of the interpretation of
		  invariants, pre- and postconditions, their transformation,
		  an executable sub-language and the possibilities of
		  refinement notions. A particular emphasize is put on the
		  issue of mechanized deduction in UML/OCL specification. },
  keywords = {OCL, Formal semantics, Constraint languages, Refinement,
		  higher-order logic},
  paddress = {Heidelberg},
  address = {Dresden},
  author = {Achim D. Brucker and Burkhart Wolff},
  classification = {conference},
  booktitle = {UML 2002: Model Engineering, Concepts and Tools},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/3-540-45800-X_17},
  language = {USenglish},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 2460,
  editor = {Jean-Marc J{\'e}z{\'e}quel and Heinrich Hussmann and
		  Stephen Cook},
  pdf = {http://www.brucker.ch/bibliography/download/2002/holocl_experiences.pdf},
  project = {CSFMDOS},
  year = 2002
}
@techreport{brucker.ea:hol-testgen:2005,
  author = {Achim D. Brucker and Burkhart Wolff},
  institution = {Computer Security Group, ETH Z\"urich},
  language = {USenglish},
  month = {apr},
  number = 482,
  title = {{HOL-TestGen} 1.0.0 User Guide},
  classification = {unrefereed},
  year = 2005,
  user = {wolff}
}
@incollection{brucker.ea: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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@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}
}
@incollection{brucker.ea:package:2006,
  author = {Achim D. Brucker and Burkhart Wolff},
  title = {A Package for Extensible Object-Oriented Data Models with
		  an Application to IMP++},
  editor = {Abhik Roychoudhury and Zijiang Yang},
  booktitle = {International Workshop on Software Verification and
		  Validation (SVV 2006)},
  year = 2006,
  series = {Computing Research Repository (CoRR)},
  month = aug,
  address = {Seattle, USA},
  language = {USenglish},
  abstract = {We present a datatype package that enables the use of
		  shallow embedding technique to object-oriented
		  specification and programming languages. The package
		  incrementally compiles an object-oriented data model to a
		  theory containing object-universes, constructors, and
		  accessor functions, coercions between dynamic and static
		  types, characteristic sets, their relations reflecting
		  inheritance, and the necessary class invariants. The
		  package is conservative, i.e., all properties are derived
		  entirely from axiomatic definitions. As an application, we
		  use the package for an object-oriented core-language called
		  \IMPOO, for which correctness of a Hoare logic with respect
		  to an operational semantics is proven.},
  categories = {holocl},
  ps = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.ps.gz},
  pdf = {http://www.brucker.ch/bibliography/download/2006/brucker.ea-package-2006.pdf},
  classification = {workshop},
  keywords = {datatype package, extensible object-oriented data model,
		  object-oriented specification,shallow embedding}
}
@incollection{brucker.ea:proposal:2002,
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-proposal-2002},
  abstract = {We present a formal semantics as a conservative shallow
		  embedding of the Object Constraint Language (OCL). OCL is
		  currently under development within an open standardization
		  process within the OMG; our work is an attempt to accompany
		  this process by a proposal solving open questions in a
		  consistent way and exploring alternatives of the language
		  design. Moreover, our encoding gives the foundation for
		  tool supported reasoning over OCL specifications, for
		  example as basis for test case generation.},
  keywords = {Isabelle, OCL, UML, shallow embedding, testing},
  paddress = {Heidelberg},
  address = {Hampton, VA, USA},
  author = {Achim D. Brucker and Burkhart Wolff},
  classification = {conference},
  booktitle = {Theorem Proving in Higher Order Logics},
  copyright = {\copyright Springer-Verlag},
  doi = {10.1007/3-540-45685-6_8},
  editor = {C{\'e}sar Mu{\~n}oz and Sophi{\`e}ne Tahar and V{\'\i}ctor
		  Carre{\~n}o},
  language = {USenglish},
  pdf = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic.pdf},
  filelabel = {extended},
  file = {http://www.brucker.ch/bibliography/download/2002/ocl_semantic_extended.pdf},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 2410,
  pages = {99--114},
  project = {CSFMDOS},
  title = {A Proposal for a Formal {OCL} Semantics in
		  {Isabelle/HOL}},
  year = 2002
}
@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}
}
@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}
}
@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}
}
@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}
}
@incollection{brucker.ea:test-sequence:2007,
  abstract = {HOL-TestGen is a specification and test-case generation
		  environment extending the interactive theorem prover
		  Isabelle/HOL. Its method is two-staged: first, the original
		  formula is partitioned into test cases by transformation
		  into a normal form. Second, the test cases are analyzed for
		  ground instances (the test data) satisfying the constraints
		  of the test cases. Particular emphasis is put on the
		  control of explicit test hypotheses which can be proven
		  over concrete programs.
		  
		  Although originally designed for black-box unit-tests,
		  HOL-TestGen's underlying logic and deduction engine is
		  powerful enough to be used in test-sequence generation, too.
		  
		  We develop the theory for test-sequence generation with
		  HOL-TestGen and describe its use in a substantial
		  case-study in the field of computer security, namely the
		  black-box test of configured firewalls. },
  keywords = {security, model-based testing, specification-based
		  testing, firewall testing},
  paddress = {Heidelberg},
  address = {Zurich},
  author = {Achim D. Brucker and Burkhart Wolff},
  booktitle = {{TAP} 2007: Tests And Proofs},
  copyright = {\copyright Springer-Verlag},
  copyrighturl = {http://link.springer-ny.com/link/service/series/0558/},
  language = {USenglish},
  publisher = {Springer-Verlag},
  series = {Lecture Notes in Computer Science},
  number = 4454,
  editor = {Bertrand Meyer and Yuri Gurevich},
  project = {CSFMDOS},
  title = {Test-Sequence Generation with HOL-TestGen -- With an
		  Application to Firewall Testing },
  categories = {holtestgen},
  classification = {conference},
  year = 2007,
  doi = {10.1007/978-3-540-73770-4_9},
  pages = {149--168},
  isbn = {978-3-540-73769-8},
  classification = {conference},
  pdf = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.pdf},
  ps = {http://www.brucker.ch/bibliography/download/2007/brucker.ea-test-sequence-2007.ps.gz},
  url = {http://www.brucker.ch/bibliography/abstract/brucker.ea-test-sequence-2007}
}
@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}
}
@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}
}
@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}
}
@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}
}
@article{brucker.rittinger.ea:hol-z,
  abstract = { We present a new proof environment for the specification
		  language Z. The basis is a semantic representation of Z in
		  a structure-preserving, shallow embedding in Isabelle/HOL.
		  On top of the embedding, new proof support for the Z schema
		  calculus and for proof structuring are developed. Thus, we
		  integrate Z into a well-known and trusted theorem prover
		  with advanced deduction technology such as higher-order
		  rewriting, tableaux-based provers and arithmetic decision
		  procedures. A further achievement of this work is the
		  integration of our embedding into a new tool-chain
		  providing a Z-oriented type checker, documentation
		  facilities and macro support for refinement proofs; as a
		  result, the gap has been closed between a logical embedding
		  proven correct and a \emph{tool} suited for applications of
		  non-trivial size.},
  author = {Achim D. Brucker and Frank Rittinger and Burkhart Wolff},
  journal = {Journal of Universal Computer Science},
  classification = {journal},
  language = {USenglish},
  title = {{HOL-Z} 2.0: {A} {P}roof {E}nvironment for {Z}-{S}pecifications},
  volume = 9,
  year = 2003,
  number = 2,
  pages = {152--172},
  month = feb,
  issn = {0948-6968},
  ps = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.ps.gz},
  pdf = {http://www.brucker.ch/bibliography/download/2003/jucs_holz_02.pdf},
  copyright = {\copyright J.UCS},
  doi = {10.3217/jucs-009-02-0152},
  copyrighturl = {http://www.jucs.org/jucs_9_2/hol_z_2}
}
@inproceedings{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}
}
@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}
}
@proceedings{garca.ea:proceedings:2006,
  abstract = {This book constitutes the refereed proceedings of the
		  International Workshop on Formal Aspects of Testing and
		  Runtime Verification, FATES/RV 2006, held in Seattle, USA
		  in August 2006 in conjuction with FLoC.The 14 revised full
		  papers presented together with twoinvited papers were
		  carefully reviewed and selected from 34 submissions. },
  address = {Seattle, USA},
  copyright = {\ Springer-Verlag},
  editor = {Manuel N{\'u}{\~n}ez Garc{\'\i}a and Klaus Havelund and
		   Grigore Rosu and Burkhart Wolff},
  copyrighturl = {http://dx.doi.org/10.1007/11940197},
  doi = {10.1007/11940197},
  language = {USenglish},
  note = {LNCS 4262.},
  publisher = {Springer Verlag},
  title = {Proceedings of the International Workshop on Formal
		  Aspects of Testing and Runtime Verification (FATES/RV)},
  year = 2006,
  classification = {workshop},
  user = {wolff}
}
@inproceedings{klmw96a,
  author = {Kolyang and C. L{\"u}th and T. Meier and B. Wolff},
  booktitle = {Proceedings of the User Interfaces for Theorem Provers
		  (UITP 96)},
  editor = {N. Merriam},
  publisher = {University of York},
  series = {Technical Report},
  title = {Generating Graphical User-Interfaces in a Functional
		  Setting},
  year = 1996,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/uitp96.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}
@inproceedings{klmw97,
  author = {Kolyang and C. L{\"u}th and T. Meier and B. Wolff},
  booktitle = {TAPSOFT 97: Theory and Practice of Software Development },
  editor = {M. Bidoit, M. Dauchet},
  pages = {855--858},
  publisher = {Springer Verlag},
  series = {LNCS 1214},
  doi = {10.1007/BFb0030646},
  title = {TAS and IsaWin: Generic Interfaces for Transformational
		  Program Development and Theorem Proving},
  year = 1997,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/tapsoft.ps.gz},
  language = {USEnglish},
  classification = {conference}
}
@inproceedings{klmw97b,
  author = {Kolyang and C. L{\"}uth and T. Meier and B. Wolff},
  booktitle = {Proceedings of the ``International Workshop for Tool
		  Support in Verification and Validation{\'{}}{\'{}}},
  editor = {K.Berghammer, J.Peleska, B. Buth},
  publisher = {Shaker Verlag},
  series = {BISS Monographs},
  title = {Generic Interfaces for Transformation Systems and
		  Interactive Theorem Provers. },
  year = 1997,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/tsv.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}
@inproceedings{klsw95,
  author = {B. Krieg-Br{\"u}ckner and J. Liu and H. Shi and B. Wolff},
  booktitle = {KORSO --- Methods, Languages, and Tools for the
		  Construction of Correct Software},
  editor = {M. Broy and S. J{\"a}hnichen},
  pages = {270--284},
  publisher = {Springer Verlag},
  series = {LNCS 1009},
  title = {Towards Correct, Efficient and Re-usable Transformational
		  Developments},
  year = 1995,
  ps = {http://www.informatik.uni-bremen.de/~bu/papers/klsw37.kurz.ps.gz},
  language = {USEnglish},
  classification = {workshop}
}
@inproceedings{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}
}
@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}
}
@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}
}
@article{luth.ea:functional:1999,
  author = {Christoph L{\"u}th and Burkhart Wolff},
  title = {Functional Design and Implementation of Graphical User
		  Interfaces for Theorem Provers},
  journal = {Journal of Functional Programming},
  year = 1999,
  volume = 9,
  number = 2,
  pages = {167-- 189},
  classification = {journal},
  doi = {10.1017/S0956796899003421},
  month = march,
  abstract = {This paper attempts to develop a metaphor suited to
		  visualize the LCF-style prover design, and a methodology
		  for the implementation of graphical user interfaces for
		  these provers and encapsulations of formal methods. In this
		  problem domain, particular attention has to be paid to the
		  need to construct a variety of objects, keep track of their
		  interdependencies and provide support for their
		  reconstruction as a consequence of changes. We present a
		  prototypical implementation of a generic and
		  open interface system architecture, and show how
		  it can be instantiated to an interface for Isabelle, called
		  IsaWin, as well as to a tailored tool for transformational
		  program development, called TAS.},
  ps = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/1999/fungui.ps.gz},
  language = {USenglish},
  pdf = {http://kisogawa.ethz.ch/WebBIB/publications-softech/papers/1999/fungui.pdf}
}
@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. }
}
@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. }
}
@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
}
@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.}
}
@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}
}
@techreport{lww96,
  author = {C. L{\"u}th and S. Westmeier and B. Wolff},
  institution = {Universit{\"a}t Bremen},
  title = {sml_tk: Functional Programming for Graphical User
		  Interfaces},
  number = {8/96},
  year = 1996,
  comment = {outdated version 2.1},
  ps = {http://www.informatik.uni-bremen.de/~cxl/sml_tk/doc/Titel.ps.gz;
		  http://www.informatik.uni-bremen.de/~cxl/sml_tk/doc/DOC.ps.gz},
  language = {USEnglish},
  classification = {unrefereed}
}
@inproceedings{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.}
}
@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}
}
@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
}
@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}
}
@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}
}
@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}
}
@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://www.lri.fr/~wolff/papers/conf/2007-tphols-isar-tool-framework.pdf},
  publisher = {Springer-Verlag},
  series = {LNCS 4732},
  title = {Building Formal Method Tools in the Isabelle/Isar Framework},
  year = 2007,
  classification = {conference},
  user = {wolff}
}
@thesis{wolff05,
  author = {Burkhart Wolff},
  title = {Correct Tools for Formal Methods in Software Engineering},
  publisher = {Universit{\"a}t Freiburg},
  year = 2005,
  language = {USEnglish},
  abstract = {The development of \emph{tools} for program analysis,
		  verification and refinement is a prerequisite for the
		  proliferation of formal methods in industry and research.
		  While most tools were directly implemented in a programming
		  language, the ultimate goal of this work is to represent
		  widely known formal methods in a so-called \emph{logical
		  framework} \textbf{by their semantics} using a particular
		  representation technique --- called \emph{shallow
		  embedding} --- motivated by more efficient deduction. Based
		  on this representation, symbolic computations in tool
		  implementations can be based on formally proven correct
		  \emph{derived rules}. As such, this correctness-oriented
		  approach has been known for a while and has been criticized
		  for a number of shortcomings: \begin{enumerate} \item the
		  application range of embeddings in logical frameworks is
		  limited to very small and artificially designed languages,
		  \item their application is impossible when the formal
		  specification method is still under development, \item
		  embedding the semantics conservatively and deriving some
		  rules on this basis does not imply that there is a
		  comprehensive support of a method that is technically
		  powerful enough for applications, \item the integration in
		  a more global software engineering process and its
		  pragmatics is too difficult, and \item the usability of
		  embeddings is doubtful even if one is targeting at the
		  (fairly small market of) proof environments.
		  \end{enumerate} In contrast to this criticism, we claim
		  that our approach is feasible. We substantiate this by
		  developing: \begin{enumerate} \item suitable embeddings for
		  widely used formal methods, including process-oriented,
		  data-oriented and object-oriented specification methods
		  (CSP, Z, UML/OCL), \item abstractions and aspect-oriented
		  structuring techniques allowing for the quick development
		  of semantic variants enabling the study consequences of
		  changes in formal methods under development (like UML/OCL),
		  \item particular techniques for generating library
		  theories, for supporting particular deduction styles in
		  proofs, for specialized deduction support for concrete
		  development methodologies, \item different scenarios of the
		  integration of the developed tools in conventional tool
		  chains in software engineering, and \item front-ends for
		  light-weight integration into tool chains (like HOL-Z 2.0)
		  or prototypic encapsulation of logical embeddings into
		  generic graphical user-interfaces for a more comprehensive
		  encapsulation. \end{enumerate} Finally, we validate one of
		  these tool chains (HOL-Z 2.0) by a substantial case-study
		  in the field of computer security. },
  note = {Habilitationsschrift},
  classification = {book},
  url = {http://www.lri.fr/~wolff/papers/other/habilschrift.pdf}
}
@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}
}
@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}
}
@inproceedings{wolff:verifying:2001,
  abstract = {Binding structures enrich traditional abstract syntax by
		  provi-ding support for representing binding mechanisms
		  (based on deBruijn indices), term-schemata and a very clean
		  algebraic theory of substitution. Weprovide a novel binding
		  structure with the following main results: 1) The
		  formalisation of a generic binding structure with the novel
		  conceptof effect-binding that enables the explicit
		  representations of both contexts and terms inside one term
		  meta-language,2) The foundation of a formal
		  (machine-assisted) substitution theory of effect-binding
		  that is well-suited for mechanisation. This can be used for
		  thesystematic and correct development of new calculi with
		  explicit substitutions.The substitution theory is formally
		  proven in Isabelle/HOL; the implementation may serve as
		  (untyped) framework for deep embeddings.},
  author = {Burkhart Wolff},
  classification = {proceedings},
  booktitle = {Workshop on Explicit Substitution Theory and Applications
		  (WESTAPP'01)},
  editor = {Pierre Lescanne},
  isbn = {90-393-2764-5},
  language = {english},
  month = {May},
  pages = {58 -- 71},
  ps = {http://kisogawa.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},
  classification = {workshop},
  volume = 210,
  year = 2001
}
@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}
}
@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
}
@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}
}
@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 = jan,
  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}
}

This file was generated by bibtex2html 1.96.