Much Ado About Two. - Sascha Böhme (Arch. Formal Proofs, 2007)

HOL-Boogie - An Interactive Prover for the Boogie Program-Verifier. - Sascha Böhme; K. Rustan M. Leino; Burkhart Wolff (TPHOLs, 2008)

Sledgehammer: Judgement Day. - Sascha Böhme; Tobias Nipkow (IJCAR, 2010)

Fast LCF-Style Proof Reconstruction for Z3. - Sascha Böhme; Tjark Weber (ITP, 2010)

HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler. - Sascha Böhme; Michal Moskal; Wolfram Schulte; Burkhart Wolff (J. Autom. Reason., 2010)

Heaps and Data Structures: A Challenge for Automated Provers. - Sascha Böhme; Michal Moskal (CADE, 2011)

Verification of Certifying Computations. - Eyad Alkassar; Sascha Böhme; Kurt Mehlhorn; Christine Rizkallah (CAV, 2011)

Reconstruction of Z3's Bit-Vector Proofs in HOL4 and Isabelle/HOL. - Sascha Böhme; Anthony C. J. Fox; Thomas Sewell; Tjark Weber (CPP, 2011)

Designing Proof Formats: A User's Perspective. - Sascha Böhme; Tjark Weber (PxTP, 2011)

An Introduction to Certifying Algorithms. - Eyad Alkassar; Sascha Böhme; Kurt Mehlhorn; Christine Rizkallah; Pascal Schweitzer (it Inf. Technol., 2011)

Proving Theorems of Higher-Order Logic with SMT Solvers. - Sascha Böhme (2012)

Extending Sledgehammer with SMT Solvers. - Jasmin Christian Blanchette; Sascha Böhme; Lawrence C. Paulson (J. Autom. Reason., 2013)

A Framework for the Verification of Certifying Computations. - Eyad Alkassar; Sascha Böhme; Kurt Mehlhorn; Christine Rizkallah (J. Autom. Reason., 2014)

Encoding Monomorphic and Polymorphic Types. - Jasmin Christian Blanchette; Sascha Böhme; Andrei Popescu 001; Nicholas Smallbone (Log. Methods Comput. Sci., 2016)

Semi-intelligible Isar Proofs from Machine-Generated Proofs. - Jasmin Christian Blanchette; Sascha Böhme; Mathias Fleury; Steffen Juilf Smolka; Albert Steckermeier (J. Autom. Reason., 2016)