Florian Kammüller, Papers/Dissertations
Most papers are as postscript sources available (gzipped). Don't hesitate to contact me if you need more information, or have problems with downloading.

Conference and Journal Publications

  • S. Preibusch and F. Kammüller. Checking the TWIN Elevator System by Translating Object-Z to SMV. Accepted at 12th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2007.
  • L. Henrio and F. Kammüller. A Mechanized Model of the Theory of Objects. Accepted at 9th IFIP International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2007. To appear in Springer LNCS.
  • F. Kammüller and S. Preibusch. An Industrial Application of Symbolic Model Checking -- The TWIN-Elevator Case Study. Accepted for publication in Informatik Forschung und Entwicklung. Springer 2007.
  • F. Kammüller and M. Vösgen. Towards Type Safety of Aspect-Oriented Languages. In Foundations of Aspect-Oriented Languages, Satellite Workshop to AOSD 06, March'06. Talk slides.
  • Steffen Helke and F. Kammüller. Property Preserving Abstraction for Statecharts. 25th IFIP WG 6.1 International Conference on Formal Techniques for Networked and Distributed Systems, FORTE 2005, Taipei, Taiwan, October 2005. LNCS, Volume 3731, 2005.
  • Florian Kammüller. Exploring New OO-Paradigms in HOL: Aspects and Collaborations TPHOLs 2005, Emerging Trends. Oxford, August 2005.
  • Florian Kammüller and J. W. Sanders. Idempotent Relations in Isabelle/HOL. First International Colloquium on Theoretical Aspects of Computing. ICTAC 2004 Guiyang, China 20 - 24 September 2004. LNCS Col. 3407, Springer 2005.
  • Florian Kammüller and J. W. Sanders. Heuristics for Refinement Relations. 2nd IEEE Int. Conf. on Software Engineering and Formal Methods SEFM04. Beijing September 2004. ISBN 0-7695-2222-X, IEEE.
  • Steffen Helke, Florian Kammüller. Verification of Statecharts Including Data Spaces. Emerging Trends of Theorem Proving in Higher Order Logics (TPHOLs 2003). Proceedings as TR No. 187 Albert-Ludwigs-Universität Freiburg, Aracne, Rome, September 2003, ISBN 88-7999-546-4,.
  • Steffen Helke, Florian Kammüller. A Framework for Property Preservation Based on Galois Connections. Emerging Trends of Theorem Proving in Higher Order Logics (TPHOLs 2003). Proceedings as TR No. 187 Albert-Ludwigs-Universität Freiburg, Aracne, Rome, September 2003, ISBN 88-7999-546-4.
  • Margot Bittner, Florian Kammueller. Translating Fusion/UML to Object-Z First ACM and IEEE International Conference on Formal Methods and Models for Codesign. (MEMOCODE'2003). ISBN 0-7695-1923-7/03, IEEE. Mt. St. Michel, France June 2003 (An extended version is RR 2003/6, see below).
  • bookreview Automated Theorem Proving in Software Engineering. J.M. Schumann, Springer Verlag. In Journal of Software Testing, Verification and Reliability (STVR), Vol 12, Number 3, p. 188-189. Wiley 2002.
  • G. Smith, F. Kammüller, T. Santen. Encoding Object-Z in Isabelle/HOL, in D. Bert, J. P. Bowen, M. C. Henson and K. Robinson (Eds.), The 2nd International Z and B Conference. Grenoble, France January 23-25, 2002. Volume 2272 of LNCS, Springer.
  • S. Helke and F. Kammüller. Representing Hierarchical Automata in Interactive Theorem Provers, in R. J. Boulton, P. B. Jackson (Eds.), Theorem Proving in Higher Order Logics, 14th International Conference, TPHOLs 2001, Edinburgh, Scotland, UK, September 3-6, 2001, Proceedings. Volume 2152 of LNCS, Springer.
  • J. Burghardt, F. Kammüller, J. W. Sanders. On the antisymmetry of Galois embeddings. Information Processing Letters, Volume 79, Issue 2, 30 June 2001. Elsevier.
  • F. Kammüller, Modular Reasoning in Isabelle, in 17th International Conference on Automated Deduction, CADE-17, June 17-20, 2000. Pittsburgh, Pennsylvania, USA. Volume 1831 of LNAI, Springer ©.
  • F. Kammüller and L. C. Paulson, A Formal Proof of Sylow's First Theorem -- An Experiment in Abstract Algebra with Isabelle HOL, Journal of Automated Reasoning , Vol. 23, Nos. 3 - 4, November 1999.
  • F. Kammüller, M. Wenzel,and L. C. Paulson, Locales -- A Sectioning Concept for Isabelle, in Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, and L. Thery (Eds.) Theorem Proving in Higher Order Logics, 12th International Conference, TPHOLs'99, Nice, France, September 14 - 17, 1999. Proceedings. Volume 1690 of LNCS, Springer ©.
  • F. Kammüller, Modular Structures as Dependent Types in Isabelle, in T. Altenkirch, W. Naraschewski, and B. Reus (Eds.), Types for Proofs and Programs International Workshop, TYPES `98, Kloster Irsee, Germany, March 27 - 31, 1998, Selected Papers. Volume 1657 of LNCS, Springer-Verlag ©.
  • F. Kammüller, G. Keller, M. Simons, and M. Weber, Structured presentation of formal proofs -- experiments with Isabelle, in L. C. Paulson, (Ed.), `Proceedings of the First Isabelle Users Workshop', Technical Report 379, Cambridge University Computer Laboratory ©, 1995.
  • T. Santen, F. Kammüller, S. Jähnichen& M. Beyer, Formalization of algebraic specification in the development language Deva , in M. Broy and S. Jähnichen (Eds.), KORSO: Methods, Languages, and Tools for the Construction of Correct Software, Volume 1009 of LNCS, Springer Verlag ©, pp. 223-238, 1995.

    • Dissertations

  • F. Kammüller, Modular Reasoning in Isabelle, PhD thesis, Computer Laboratory, University of Cambridge, Technical Report 470 . August, 1999.
  • F. Kammüller, Experimental support of a proof programming language with Isabelle. Diplomarbeit, Technical University Berlin, 1995.
  • F. Kammüller, Lazy lists as a case study of constructing datatypes, Studienarbeit, TU-Berlin, Fachbereich Informatik, 1994.

    • Technical Reports

  • Ludovic Henrio and F. Kammüller. A Formalization of the Theory of Objects in Isabelle/HOL. Technical Report RR-6079, INRIA Sophia-Antipolis, 2006.
  • F. Kammüller and J.W. Sanders. Idempotent Relations in Isabelle/HOL. Technische Universität Berlin, Rote Reihe, 2004/04.
  • M. Bittner and F. Kammüller. Controlling Consistency in UML with Fusion and Object-Z. Technische Universität Berlin, Rote Reihe, 2003/06.
  • J. Burghardt, F. Kammüller, and J. W. Sanders, Isomorphism of Galois Embeddings, GMD Report 122, 74 pages. Dezember 2000.
  • F. Kammüller and L. C. Paulson, A Formal Proof of Sylow's First Theorem -- An Experiment in Abstract Algebra with Isabelle HOL, Technical Report 452 , Computer Laboratory, University of Cambridge. October 1998. ©).
  • F. Kammüller and M. Wenzel. Locales -- A Sectioning Concept for Isabelle. TR 449 Computer Laboratory, University of Cambridge. November 1998. ©.

    • Others

  • F. Kammüller. Number of Labelled Idempotents. Entry in the On-Line Encyclopedia of Integer Sequences.
  • S. Helke, F. Kammüller, J. W. Sanders. Synthesizing Refinements from Predicate Translations. Dagstuhl Seminar Nº 359, 2002.
  • G. Smith, F. Kammüller, T. Santen. Formalizing Reference Semantics of Object-Z in Isabelle/HOL. Can Formal Methods Cope with Software Intensive Systems. Dagstuhl Seminar Nº 01221, May 2001. Dagstuhl-Seminar-Report Nº 308.
  • F. Kammüller and S. Helke. Mechanical Analysis of UML State Machines and Class Diagrams. Workshop on Precise Semantics for the UML. ECOOP2000, Cannes, June 2000.
  • F. Kammüller, M. Wenzel,and L. C. Paulson. Locales, A Sectioning Concept for Isabelle. Rigorous Analysis and Design for Software Intensive Systems, November 1999. Dagstuhl Seminar Nº 99451, Dagstuhl-Seminar-Report Nº 258.
  • F. Kammüller, Comparison of IMPS, PVS and Larch with respect to Theory Treatment and Modularization, Unpublished Draft, 1996.

    © Copyright Notice: The documents distributed by this server have been provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a noncommercial 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.

    Last modified: March 2007