Fabian Immler

Since July 2020, I work as a Formal Verification Engineer at Apple.

eMail:	fabian.immler gmail.com

From July 2018 to June 2020 I was a Post-Doctoral 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 higher-order 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, HOL-ODE-Numerics.
• December 2018: "Heinz Schwärtzel-Dissertationspreis 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
• RIPEMD-160.
  Fabian Immler
  Archive of Formal Proofs

Workshops

• ARCH-COMP19 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)
• ARCH-COMP18 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)
• ARCH-COMP17 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.