1. Mike Barnett, Bor-Yuh Evan Chang, Robert DeLine, Bart Jacobs & K. Rustan M. Leino (2006): Boogie: A Modular Reusable Verifier for Object-Oriented Programs. In: Frank S. de Boer, Marcello M. Bonsangue, Susanne Graf & Willem-Paul de Roever: Formal Methods for Components and Objects (FMCO), LNCS 4111. Springer, pp. 364–387. Available at
  2. Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte & Herman Venter (2011): Specification and Verification: The Spec# Experience. Communications of the ACM 54(6), pp. 81–91. Available at
  3. Jasmin Christian Blanchette & Tobias Nipkow (2010): Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder. In: Matt Kaufmann & Lawrence C. Paulson: Interactive Theorem Proving (ITP), LNCS 6172. Springer, pp. 131–146. Available at
  4. François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond & Andrei Paskevich (2013): Preserving User Proofs across Specification Changes. In: Ernie Cohen & Andrey Rybalchenko: VSTTE, LNCS 8164. Springer, pp. 191–201. Available at
  5. Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, MichałMoskal, Thomas Santen, Wolfram Schulte & Stephan Tobies (2009): VCC: A Practical System for Verifying Concurrent C. In: Stefan Berghofer, Tobias Nipkow, Christian Urban & Makarius Wenzel: Theorem Proving in Higher Order Logics (TPHOLs), LNCS 5674. Springer, pp. 23–42. Available at
  6. David R. Cok (2010): Improved usability and performance of SMT solvers for debugging specifications. Software Tools for Technology Transfer (STTT) 12(6), pp. 467–481. Available at
  7. David R. Cok (2014): OpenJML: Software verification for Java 7 using JML, OpenJDK, and Eclipse. In: Catherine Dubois, Dimitra Giannakopoulou & Dominique Méry: 1st Workshop on Formal-IDE.
  8. Claire Dross, Pavlos Efstathopoulos, David Lesens, David Mentré & Yannick Moy (2014): Rail, Space, Security: Three Case Studies for SPARK 2014. In: 7th Europen Congress on Embedded Real Time Software and Systems (ERTS^2 2014). Available at
  9. Jean-Christophe Filliâtre & Andrei Paskevich (2013): Why3 — Where Programs Meet Provers. In: Matthias Felleisen & Philippa Gardner: European Symposium on Programming (ESOP), LNCS 7792. Springer, pp. 125–128. Available at
  10. Claire Le Goues, K. Rustan M. Leino & MichałMoskal (2011): The Boogie Verification Debugger (Tool Paper). In: Gilles Barthe, Alberto Pardo & Gerardo Schneider: Software Engineering and Formal Methods (SEFM), LNCS 7041. Springer, pp. 407–414. Available at
  11. Radu Grigore & MichałMoskal (2007): Edit and Verify. In: Workshop on First-Order Theorem Proving (FTP). Available at
  12. Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000): Computer-Aided Reasoning: An Approach. Kluwer Academic Publishers.
  13. Vladimir Klebanov (2009): Extending the Reach and Power of Deductive Program Verification. Department of Computer Science, Universität Koblenz-Landau. Available at
  14. Jason Koenig & K. Rustan M. Leino (2012): Getting Started with Dafny: A Guide. In: Tobias Nipkow, Orna Grumberg & Benedikt Hauptmann: Software Safety and Security: Tools for Analysis and Verification, NATO Science for Peace and Security Series D: Information and Communication Security 33. IOS Press, pp. 152–181. Available at Summer School Marktoberdorf 2011 lecture notes. A version of this tutorial is available online at
  15. K. Rustan M. Leino (2009): Specification and verification of object-oriented software. In: Manfred Broy, Wassiou Sitou & Tony Hoare: Engineering Methods and Tools for Software Safety and Security, NATO Science for Peace and Security Series D: Information and Communication Security 22. IOS Press, pp. 231–266. Available at Summer School Marktoberdorf 2008 lecture notes.
  16. K. Rustan M. Leino (2010): Dafny: An Automatic Program Verifier for Functional Correctness. In: Edmund M. Clarke & Andrei Voronkov: Logic for Programming Artificial Intelligence and Reasoning (LPAR), LNCS 6355. Springer, pp. 348–370. Available at
  17. K. Rustan M. Leino (2012): Automating Induction with an SMT Solver. In: Viktor Kuncak & Andrey Rybalchenko: Verification, Model Checking, and Abstract Interpretation (VMCAI), LNCS 7148. Springer, pp. 315–331. Available at
  18. K. Rustan M. Leino & MichałMoskal (2013): Co-induction Simply: Automatic Co-inductive Proofs in a Program Verifier. Technical Report MSR-TR-2013-49. Microsoft Research. Available at
  19. K. Rustan M. Leino, MichałMoskal & Wolfram Schulte (2008): Verification Condition Splitting. Technical Report. Microsoft Research. Available at Manuscript KRML 192.
  20. K. Rustan M. Leino & Philipp Rümmer (2010): A Polymorphic Intermediate Verification Language: Design and Logical Encoding. In: Javier Esparza & Rupak Majumdar: Tools and Algorithms for the Construction and Analysis of Systems, 16th International Conference, TACAS 2010, LNCS 6015. Springer, pp. 312–327. Available at
  21. Leonardo de Moura & Nikolaj Bjørner (2008): Z3: An Efficient SMT Solver. In: C. R. Ramakrishnan & Jakob Rehof: Tools and Algorithms for Construction and Analysis of Systems (TACAS), LNCS 4963. Springer, pp. 337–340. Available at
  22. Wolfgang Reif & Kurt Stenzel (1993): Reuse of Proofs in Software Verification. In: R. K. Shyamasundar: Foundations of Software Technology and Theoretical Computer Science, LNCS 761. Springer, pp. 284–293. Available at
  23. Christian Sternagel (2012): Getting Started with Isabelle/jEdit. In: Isabelle Users Workshop (IUW). Available at
  24. Makarius Wenzel (2010): Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. In: 9th International Workshop On User Interfaces for Theorem Provers (UITP 2010), Electronic Notes in Theoretical Computer Science. Elsevier. Available at

Comments and questions to:
For website issues: