I studied computer science, with mathematics as minor subject, at the TU München since 2004. Since May 2009 I'm a graduate student as part of the PUMA graduate school.
| Address [vCard]: |
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 01.11.057![[MI 01.11.057]](images/room-location.jpeg)
|
My interests are mainly formalizing mathematics in higher-order logic and verifying software upon this. My current work mostly is related to the Isabelle theorem prover.
Wir müssen wissen,
wir werden wissen.
-
David Hilbert
Publications
Conferences
- Verifying pCTL Model Checking.
Johannes Hölzl and Tobias Nipkow.
Proceedings of the TACAS '12. BibTex
(The original publication is available at www.springerlink.com) - Three Chapters of Measure Theory.
Johannes Hölzl and Armin Heller.
Proceedings of the ITP '11 (LNCS 6898). BibTex
(The original publication is available at www.springerlink.com) - Specifying and
Verifying Sparse Matrix Codes.
Gilad Arnold, Johannes Hölzl, Ali Sinan Köksal, Rastislav Bodík, and Mooly Sagiv.
Proceedings of the ICFP '10. (© ACM) BibTex - Proving Inequalities over Reals with Computation
in Isabelle/HOL.
Johannes Hölzl.
Proceedings of the PLMMS '09 (© ACM) Slides BibTex
Diploma thesis
-
Proving Real-Valued Inequalities by Computation
in Isabelle/HOL.
Diploma thesis. Institut für Informatik, TU München. April 2009. BibTex
Current Work
- Measure, Probability, and Information
- Together with Armin Heller I formalized the first three chapters of Heinz Bauer's textbook about measure theory. This is now officially part of the Isabelle repository. We built on the work from Aaron Coble which was ported to Isabelle by Lawrence C. Paulson.
- Multivariate Analysis
- Robert Himmelmann is currently porting the formalization of Multivariate Analysis available in HOL Light. The current development is found in the Isabelle repository.
- Up Down
- I'm working together with Dirk Pflüger on the publication of the verification of the up-down algorithm.
Past Work
- Verification of Sparse Matrix codes
- Gilad Arnold and I are working on automatically verifying the correctness of Sparse Matrix codes.
- Diploma thesis
- Proving Real-Valued Inequalities by Computation in Isabelle/HOL
- SEP
- Developing Isabelle user interface components for interactive Prover-IDEs based on jEdit. This is the origin of isabelle-jedit.
- IDP
- Verifying the up-down algorithm