Since July 2020, I work as a Formal Verification Engineer at Apple.
eMail:  immler in.tum.de 

From July 2018 to June 2020 I was 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
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.
News
 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.
Publications
Ph.D. Thesis

A Verified ODE Solver and Smale's 14th Problem .
Ph.D. thesis. Institut für Informatik, TU München. 2018. (official publication)
Journal Articles
 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)
Conference Proceedings

The PoincaréBendixson Theorem in Isabelle/HOL.
Fabian Immler, Yong Kiam Tan.
CPP 2020 : The 9th ACM SIGPLAN International Conference on Certified Programs and Proofs
doi, to appear 
Virtualization of HOL4 in Isabelle.
Fabian Immler, Jonas Rädle, Makarius Wenzel.
ITP 2019: Interactive Theorem Proving
doi 
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)
Formal Proofs
 The PoincaréBendixson Theorem.
Fabian Immler, Yong Kiam Tan.
Archive of Formal Proofs  Laplace Transform.
Fabian Immler.
Archive of Formal Proofs  Smooth Manifolds.
Fabian Immler, Bohua Zhan.
Archive of Formal Proofs  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
Workshops
 ARCHCOMP19 Category Report: Continuous and Hybrid Systems with Nonlinear Dynamics.
Fabian Immler, Matthias Althoff, Luis Benet, Alexandre Chapoutot, Xin Chen, Marcelo Forets, Luca Geretti, Niklas Kochdumper, David P. Sanders and Christian Schilling
ARCH19. 6th International Workshop on Applied Verification of Continuous and Hybrid Systems.
(EasyChair Proceedings in Computing, volume 61)  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
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.
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.