Sascha Böhme
boehmes  in.tum.de |
I have left TUM in October 2011 and moved on to new shores.
Journal Article
- 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-144, February 2010.
Conference Papers
- Sascha Böhme, Anthony C. J. Fox, Thomas Sewell, and Tjark Weber. Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. In Certified Programs and Proofs, 2011. To appear.
- Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. In Nikolaj Børner and Viorica Sofronie-Stokkermans, editors, Automated Deduction, volume 6803 of Lecture Notes in Computer Science, pages 116-130. Springer, 2011.
- Sascha Böhme and Michał Moskal. Heaps and Data Structures: A Challenge for Automated Provers. In Nikolaj Børner and Viorica Sofronie-Stokkermans, editors, Automated Deduction, volume 6803 of Lecture Notes in Computer Science, pages 177-191. Springer, 2011.
- Eyad Alkassar, Sascha Böhme, Kurt Mehlhorn, and Christine Rizkallah. Verification of Certifying Computations. In Ganesh Gopalakrishnan and Shaz Qadeer, editors, Computer Aided Verification, volume 6806 of Lecture Notes in Computer Science, pages 67-82. Springer, 2011.
- Sascha Böhme and Tobias Nipkow. Sledgehammer: Judgement Day. In Jürgen Giesl and Reiner Hähnle, editors, Automated Reasoning, volume 6173 of Lecture Notes in Computer Science, pages 107-121. Springer, 2010.
- Sascha Böhme and Tjark Weber. Fast LCF-Style Proof Reconstruction for Z3. In Matt Kaufmann and Lawrence Paulson, editors, Interactive Theorem Proving, volume 6172 of Lecture Notes in Computer Science, pages 179-194. Springer, 2010.
- 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, volume 5170 of Lecture Notes in Computer Science, pages 150-166. Springer, 2008.
Workshop Paper
- Sascha Böhme and Tjark Weber. Designing Proof Formats: A User's Perspective. In Proof eXchange for Theorem Proving, 2011. Accepted.
- Sascha Böhme. Proof Reconstruction for Z3 in Isabelle/HOL. In Satisfiability Modulo Theories, 2009.
Thesis
- Sascha Böhme. Proving Theorems of Higher-Order Logic with SMT Solvers. Dissertation, Technische Universität München, 2012.
Other Publications
- 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.
Program Committee
- PC member of PxTP-2011
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.
Teaching
- Einführung in die Theoretische Informatik, summer semester 2011
- Semantics of Programming Languages, winter semester 2010/2011
Projects
- HOL-Boogie
- How to run Z3 under Mac OS X?
- Python binding to Z3