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, Michał Moskal, Wolfram Schulte, and Burkhart Wolff. HOL-Boogie — An Interactive Prover-Backend for the Verifying C Compiler. Journal of Automated Reasoning, 44(1-2):111-114, February 2010.
• Sascha Böhme. Proof Reconstruction for Z3 in Isabelle/HOL. Satisfiability Modulo Theories, 2009.
• 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.
• Sascha Böhme. Free Theorems for Sublanguages of Haskell. Master's thesis, Technische Universität Dresden, 2007.

Talks

• Efficient Proof Reconstruction for the SMT Solver Z3, Talk given at Third Workshop on Formal and Automated Theorem Proving, Belgrade, Serbia, January 2010.
• 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