Since July 2018, I am a PostDoctoral Fellow in the Logical Systems Lab @ Carnegie Mellon University
My research interests are along the following lines
 reachability analysis and differential dynamic logic
 theorem prover interoperability: HOL4/Isabelle/KeYmaeraX
 formal verification of validated numerical methods, in particular for solving ordinary differential equations
 formalization of mathematics in higherorder logic
 interactive theorem proving
 April 2019: The ARCH 2019 Best Result Award was awarded to my collection of formally verified algorithms for reachability analysis of (nonlinear) systems, HOLODENumerics.
 December 2018: "Heinz SchwärtzelDissertationspreis für Grundlagen der Informatik" was awarded to my PhD thesis.
 August 2018: Best paper and best presentation (by Alexander Maletzky) for Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL at CICM 2018.

A Verified ODE Solver and Smale's 14th Problem .
Ph.D. thesis. Institut für Informatik, TU München. 2018. (official publication)
 A Verified ODE Solver and the Lorenz Attractor.
Fabian Immler.
Journal of Automated Reasoning (2018) 61
(The original publication is available (open access) at Springer Link)  The Flow of ODEs  Formalization of Variational Equation and Poincaré Map (draft).
Fabian Immler and Christoph Traut.
Journal of Automated Reasoning (2018)
(The original publication is available at Springer Link) 
Virtualization of HOL4 in Isabelle (draft).
Fabian Immler, Jonas Rädle, Makarius Wenzel.
ITP 2019: Interactive Theorem Proving
to appear 
Smooth manifolds and types to sets for linear algebra in Isabelle/HOL.
Fabian Immler, Bohua Zhan.
CPP 2019  The 8th ACM SIGPLAN International Conference on Certified Programs and Proofs
doi  A Formally Verified Motion Planner for Autonomous Vehicles
.
Albert Rizaldi, Fabian Immler, Bastian Schürmann, Matthias Althoff
Automated Technology for Verification and Analysis(ATVA 2018) (LNCS 11138)
(The original publication is available at www.springerlink.com) 
Gröbner Bases of Modules and Faugère's F4 Algorithm in Isabelle/HOL.
Alexander Maletzky, Fabian Immler
Intelligent Computer Mathematics (CICM 2018) (LNCS 11006)
(The original publication is available at www.springerlink.com)
 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)  Taylor Models.
Christoph Traut, Fabian Immler.
Archive of Formal Proofs  Gröbner Bases Theory.
Fabian Immler, Alexander Maletzky.
Archive of Formal Proofs  Ordinary Differential Equations.
Fabian Immler, Johannes Hölzl.
Archive of Formal Proofs  Affine Arithmetic.
Fabian Immler
Archive of Formal Proofs  RIPEMD160.
Fabian Immler
Archive of Formal Proofs  ARCHCOMP18 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.
Fabian Immler, Matthias Althoff, Xin Chen, Chuchu Fan, Goran Frehse, Niklas Kochdumper, Yangge Li, Sayan Mitra, Mahendra Singh Tomar, and Majid Zamani
(EasyChair Proceedings in Computing, volume 54) ARCH18. 5th International Workshop on Applied Verification of Continuous and Hybrid Systems.
(EasyChair Proceedings in Computing, volume 54)  ARCHCOMP17 Category Report: Continuous Systems with Nonlinear Dynamics.
Xin Chen, Matthias Althoff, Fabian Immler.
(EasyChair Proceedings in Computing, volume 48) 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) 
Generic Construction of Probability Spaces for
Paths of Stochastic Processes.
Master's thesis. Institut für Informatik, TU München. October 2012.
Address: 
Computer Science Department, Carnegie Mellon University 5000 Forbes Avenue, Pittsburgh, PA 15213, USA 

Telephone:  +1 (412)2688911 
Office:  Gates Hillman Center 9004 
eMail:  fimmler cs.cmu.edu 
I defended my Ph.D. on A Verified ODE Solver and Smale's 14th Problem in May 2018.
Starting in November 2012, I was a Ph.D. student as part of the PUMA graduate school and working on the DFG Kosseleck project Verified Algorithm Analysis. I studied computer science (B.Sc. and M.Sc.), with mathematics as minor subject, at TU München since 2007.