Major Journal Publications

Achim D. Brucker, Frederic Tuong and Burkhart Wolff: Model Transformation as Conservative Theory-Transformation. In: Journal of Object Technolology. DOI: 10.5381/jot.2020.19.3.a3. Volume 19, Issue 3, pages 1-16, September 2020.
Abderrahmane Feliachi, Marie-Claude Gaudel, and Burkhart Wolff: Symbolic Test-Generation in HOL-TestGen/Cirta: A Case Study. In: Int. J. Software Informatics. Web: Festschrift to the 66th Anniversaey of Bernd Krieg-Brueckner.. Volume 9, Issue 1, pages 177-203, September 2015.
Achim D. Brucker, Lukas Brügger and Burkhart Wolff: Formal Firewall Conformance Testing - An Application of Test and Proof Techniques . In: Software Testing, Verification and Reliability (STVR). DOI: 10.1002/stvr.1544.. Wiley InterScience (, Volume 25, Issue 1,pages 34-71, January 2015.
Achim D. Brucker and Burkhart Wolff: On Theorem Prover-based Testing. In: Formal Aspects of Computing (FAOC). DOI: 10.1007/s00165-012-0222-y. Volume 25, Issue 5, pp 683-721. Springer, September 2013.
Sascha Böhme, Michal Moskal, Wolfram Schulte and Burkhart Wolff: HOL-Boogie - An Interactive Prover-Backend for the Verified C Compiler. In Jacques Carette, Makarius Wenzel, Freek Wiedijk(Guest Editors) : Journal of Automated Reasoning (JAR), DOI: 10.1007/s10817-009-9142-9. 44(1--2), pages 111-144. Springer, 2010.
Achim D. Brucker and Burkhart Wolff: Semantics, Calculi, and Analysis for Object-Oriented Specifications. In Ernst-Rüdiger Olderog (Managing Editor): Acta Informatica. DOI: 10.1007/s00236-009-0093-8. 46 (4), pages 255-284. Springer, 2009.
Matthias Daum, Jan Dörrenbächer and Burkhart Wolff: Proving Fairness and Implementation Correctness of a Microkernel Scheduler. In: G. Klein, R. Huuck and B. Schlich: Special Issue on Operating System Verification (2009), Journal of Automated Reasoning (JAR), DOI: 10.1007/s10817-009-9119-8. 42 (2-4), pages 349-388. Springer, 2009.
Achim Brucker and Burkhart Wolff: An Extensible Encoding of Object-oriented Data Models in HOL with an Application to IMP++. In: Journal of Automated Reasoning (JAR), DOI: 10.1007/s10817-008-9108-3, 41 (3-4), pages 219-249, Springer. 2008.
David Basin and Hironobu Kuruma and Shin Nakajima and Burkhart Wolff. The Z Specification Language and the Proof Environment Isabelle/HOL-Z. In Computer Software - Journal of the Japan Society for Software Science and Technology (JSSST), 24 (2), pages 21-26, 2007. In Japanese.
David Basin, Hironobu Kuruma, Kunihiko Miyazaki, Kazuo Takaragi and Burkhart Wolff: Verifying a Signature Architecture - A Comparative Case Study. In: Formal Aspects of Computing (FAC), 19 (1), pages 63-91, Springer. DOI 10.1007/s00165-006-0012-5, 2007.
Achim D. Brucker and Burkhart Wolff: A Verification-Approach for Applied System Security. In International Journal of Software Technology and Technology Transfer (STTT), 7(5), pages 233-247. DOI 10.1007/s10009-004-0176-3, Springer, 2005.
Christoph Lüth and Burkhart Wolff: Functional Design and Implementation of Graphical User Interfaces for Theorem Provers. In Journal of Functional Programming (JFP), DOI: 10.1017/S0956796899003421,Vol 9, pages 165-189, 1999.

e-Journal and Archive Articles

Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff and Cyril Proch: Using Isabelle/HOL in Certification Processes: A System Description and Mandatory Recommendations. ISSN 2150-914x. In: EU Project EURO-MILS: Secure European Virtualisation for Trustworthy Applications in Critical Domains. Deliverable: Used Formal Methods. The latter appeared meanwhile as book (DOI: and the "Mandatory Recommendations" therefore as book chapter.
Achim D. Brucker, Lukas Brügger and Burkhart Wolff: The Unified Policy Framework (UPF). ISSN 2150-914x. Archive of Formal Proofs, Nov. 2014.
Freek Verbeek, Sergey Tverdyshev, Oto Havle, Holger Blasum, Bruno Langenstein, Werner Stephan, Yakoub Nemouchi, Abderrahmane Feliachi, Burkhart Wolff, Julien Schmaltz: Formal Specification of a Generic Separation Kernel. Archive of Formal Proofs, July 2014.
Achim D. Brucker, Frédéric Tuong, and Burkhart Wolff. Featherweight OCL: A proposal for a machine-checked formal semantics for ocl 2.5. Formal proof development. Archive of Formal Proofs, January 2014. Revised Version Sept 2015
Abderrahmane Feliachi, Burkhart Wolff, Marie-Claude Gaudel: Isabelle/Circus. Archive of Formal Proofs, July 2012.
Achim Brucker, Jürgen Doser, and Burkhart Wolff: Semantic Issues of OCL: Past, Present, and Future. In Electronic Communications of the EASST (EC-EASST), Vol 5, 20 pages, 2006.
Achim Brucker, Jürgen Doser, and Burkhart Wolff: An MDA Framework Supporting OCL. In Electronic Communications of the EASST (EC-EASST), Vol 5, 18 pages, 2006.
Achim D. Brucker, Frank Rittinger and Burkhart Wolff: HOL-Z 2.0: A Proof Environment for Z-Specifications. In Journal of Universal Computer Science (JUCS), 9 (2), pages 152-172, DOI: 10.3217/jucs-009-02-0152 , 2003.



Co-authors & co-editors

  • David Aspinal
  • Bruno Barras
  • David A. Basin
  • Sascha Böhme
  • Achim D. Brucker
  • Lukas Brügger
  • Matthias Daum
  • Jan Dörrenbächer
  • Jürgen Doser
  • Abderrahmane Feliachi
  • Marie-Claude Gaudel
  • Lourdes Del Carmen González-Huesca
  • Hugo Herbelin
  • Thierry Jéron
  • Klaus Havelund
  • Einar W. Karlsen
  • Paul Kearney
  • Alexander Knapp
  • Kolyang
  • Matthias Krieger
  • Bernd Krieg-Brückner
  • Hironobu Kuruma
  • Rustan Leino
  • Junbo Liu
  • Delphine Longuet
  • Christoph Lüth
  • Thomas Meyer
  • Michal Moskal
  • Kunihiko Miyazaki
  • Manuel Núñez
  • Yakoub Nemouchi
  • Nicole Rauch
  • Yann Régis-Gianas
  • Frank Rittinger
  • Grigore Rosu
  • Thomas Santen
  • Mareike Schmidt
  • Wolfram Schulte
  • Hui Shi
  • Kazuo Takaragi
  • Enrico Tassi
  • Haykal Tej
  • Margus Veanes
  • Makarius Wenzel
  • Stefan Westmeier
  • Fatiha Zaïdi

Copyright notice. The documents available from this site are provided as a means to ensure timely dissemination of technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder (Springer-Verlag for works appeared in the LNCS series, ACM-SIAM, IEEE, etc.). Permission to make digital or hard copies of part or all of these works for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage. The electronic version of some of the works available from this site may differ from the definitive published version. Copyright of works submitted for publication may be transferred without further notice and this version may no longer be accessible.