I am a member of the Theorem Proving Group headed by Tobias Nipkow. My research interests are centred around the interactice theorem prover Isabelle. Currently I am integrating tools to verify imperative programs in Isabelle. This also includes enriching the power of Isabelle by bindings to various SMT solvers. I am a member of the project Verisoft XT and affiliated student of PUMA.

Publications

• Sascha Böhme. Proof Reconstruction for Z3 in Isabelle/HOL. Satisfiability Modulo Theories, 2009.
• Sascha Böhme, Michał Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie — An Interactive Prover-Backend for the Verifying C Compiler. Journal of Automated Reasoning, 2009. To appear.
• Sascha Böhme, K. Rustan M. Leino, and Burkhart Wolff. HOL-Boogie—An Interactive Prover for the Boogie Program-Verifier. In Otmane Ait Mohamed, César Muñoz, and Sofiène Tahar, editors, Theorem Proving in Higher Order Logics, pages 150-166. Springer, 2008.

Other Works

• Sascha Böhme. Much Ado About Two. In Gerwin Klein, Tobias Nipkow, and Lawrence Paulson, editors, The Archive of Formal Proofs. November 2007, Formal proof development.

Talks

• Isabelle/HOL and SMT, Talk given at Laboratoire d'Informatique de l'Ecole Polytechnique, France, September 2009.

Projects

• HOL-Boogie
• How to run Z3 under Linux or Mac OS X?
• Python binding to Z3

Contact

Technische Universität München Fakultät für Informatik Boltzmannstraße 3 85748 Garching Germany

E-mail: boehmes in.tum.de Phone: +49 (89) 289-17330 Fax: +49 (89) 289-17307 Office: MI 01.11.057