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

Journal Articles

• The Flow of ODEs - Formalization of Variational Equation and Poincaré Map (draft).
  Fabian Immler and Christoph Traut.
  Accepted in Journal of Automated Reasoning
  

Conference Proceedings

• Formalising and Monitoring Traffic Rules for Autonomous Vehicles in Isabelle/HOL .
  Albert Rizaldi, Jonas Keinholz, Monika Huber, Jochen Feldle, Fabian Immler, Matthias Althoff, Eric Hilgendorf, Tobias Nipkow
  integrated Formal Methods 2017 (iFM 2017) (LNCS 10510)
  (The original publication is available at www.springerlink.com)
• The Flow of ODEs.
  Fabian Immler and Christoph Traut.
  Interactive Theorem Proving 2016 (ITP 2016) (LNCS 9807)
  (The original publication is available at www.springerlink.com)
• A Formally Verified Checker of the Safe Distance Traffic Rules for Autonomous Vehicles .
  Albert Rizaldi, Fabian Immler, Matthias Althoff.
  NASA Formal Methods Symposium 2016 (NFM 2016) (LNCS 9690)
  (The original publication is available at www.springerlink.com)
• 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)

Formal Proofs

• Ordinary Differential Equations.
  Fabian Immler, Johannes Hölzl.
  Archive of Formal Proofs
• Affine Arithmetic.
  Fabian Immler
  Archive of Formal Proofs

Workshops

• ARCH-COMP17 Category Report: Continuous Systems with Nonlinear Dynamics.
  Xin Chen, Matthias Althoff, Fabian Immler.
  (EasyChair Proceedings in Computing, volume 34) ARCH17. 4th International Workshop on Applied Verification of Continuous and Hybrid Systems.
  (EasyChair Proceedings in Computing, volume 48)
• 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.