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.
in.tum.de