Fabian Immler

Chair for Logic and Verification

I studied computer science, with mathematics as minor subject, at the TU München since 2007. Since November 2012 I am a Ph.D. student as part of the PUMA graduate school.

Address:	Fabian Immler Technische Universität München Institut für Informatik Boltzmannstr. 3 85748 Garching Deutschland
Telephone:	+49 (89) 289-17330
Telefax:	+49 (89) 289-17307
Office:	MI 00.09.061
eMail:	immler in.tum.de

My interests are in interactive theorem proving and especially formalizing mathematics in higher-order logic. I currently work on the verification of validated numerical methods, in particular for solving ordinary differential equations.

Publications

Conferences

• The Flow of ODEs (draft).
  Fabian Immler and Christoph Traut.
  To appear at Interactive Theorem Proving 2016 (ITP 2016)
  
• A Verified Enclosure for the Lorenz Attractor (Rough Diamond).
  Fabian Immler.
  Interactive Theorem Proving 2015 (ITP 2015) (LNCS 9236)
  (The original publication is available at www.springerlink.com)
• Verified Reachability Analysis of Continuous Systems.
  Fabian Immler.
  TACAS 2015 (LNCS 9035)
  (The original publication is available at www.springerlink.com)
• A Verified Algorithm for Geometric Zonotope/Hyperplane Intersection.
  Fabian Immler.
  CPP '15: Proceedings of the 2015 Conference on Certified Programs and Proofs
  doi
• Formally Verified Computation of Enclosures of Solutions of Ordinary Differential Equations.
  Fabian Immler.
  Proceedings of the 6th NASA Formal Methods Symposium (NFM 2014) (LNCS 8430).
  (The original publication is available at www.springerlink.com)
• Type Classes and Filters for Mathematical Analysis in Isabelle/HOL.
  Johannes Hölzl, Fabian Immler, and Brian Huffman.
  Proceedings of the Interactive Theorem Proving 2013 (ITP '13) (LNCS 7998).
  (The original publication is available at www.springerlink.com)
• Numerical Analysis of Ordinary Differential Equations in Isabelle/HOL.
  Fabian Immler and Johannes Hölzl.
  Proceedings of the Interactive Theorem Proving 2012 (ITP '12) (LNCS 7406).
  (The original publication is available at www.springerlink.com)

Workshops

• Tool Presentation: Isabelle/HOL for Reachability Analysis of Continuous Systems.
  Fabian Immler.
  Tool Presentation at ARCH 2015: Applied Verification for Continuous and Hybrid Systems.
  (EasyChair Proceedings in Computing, volume 34)

Master's thesis

• Generic Construction of Probability Spaces for Paths of Stochastic Processes.
  Master's thesis. Institut für Informatik, TU München. October 2012.