Fabian Immler - Logical Systems Lab - Carnegie Mellon University

Since July 2018, I am 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

Address:	Computer Science Department, Carnegie Mellon University 5000 Forbes Avenue, Pittsburgh, PA 15213, USA
Telephone:	+1 (412)-268-8911
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.

News

• 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

• 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

• 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-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
  (EasyChair Proceedings in Computing, volume 54) 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.
  (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)

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.