Fields of interest 

• Computer-Aided Theorem Proving (Isabelle)

 
• Proof Carrying Code (VeryPCC)

 
• Formal Specification Techniques

Publications

• Verified Proof Carrying Code
  Martin Wildmoser; Ph.D. thesis; Technische Universtaet Muenchen; submitted Nov. 2005; 210 pages [bibtex]



• Bytecode Analysis for Proof Carrying Code
  Martin Wildmoser, Amine Chaieb, Tobias Nipkow; Proceedings of the First Workshop on Bytecode Semantics, Verification, Analysis and Transformation (BYTECODE 2005), to appear in Electronic Notes in Computer Science (ENTCS); 15 pages [bibtex]



• Asserting Bytecode Safety
  Martin Wildmoser, Tobias Nipkow; Proceedings of the 15th European Symposium on Programming 2005 (ESOP'05); 16 pages [bibtex]



• Certifying Machine Code Safety: Shallow versus Deep Embedding
  Martin Wildmoser, Tobias Nipkow; Proceedings of the 17th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'04); (c) Springer-Verlag; 16 pages [bibtex]



• Prototyping Proof Carrying Code
  Wildmoser M.,Nipkow T.,Klein G.,Nanz S.; Exploring New Frontiers in Theoretical Informatics, 3rd IFIP Int. Conf. on Theoretical Computer Science (TCS2004); 14 pages [bibtex]



• Verified Bytecode Subroutines
  Klein G., Wildmoser M.; Proceedings of the 16th International Conference on Theorem Proving in Higher Order Logics (TPHOLs'03); (c) Springer-Verlag; 16 pages [bibtex]



• Verified Bytecode Subroutines
  Klein G., Wildmoser M.; Journal of Automated Reasoning, 2003; 38 pages [bibtex]



• Subroutines and Java Bytecode Verification
  Wildmoser M.; Diploma Thesis; 171 pages; submitted June 2002

Teaching

• Spezifikation und Verifikation
  Praktikum SS 2005
• Mathematische und logische Perlen der Informatik
  Proseminar WS 04/05
• Spezifikation und Verifikation
  Praktikum SS 2004
• Spezifikation und Verifikation
  Praktikum WS 03/04
• Spezifikation und Verifikation
  Praktikum SS 2003
• Software-Desaster
  Proseminar WS 02/03