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 http://dx.doi.org/10.1007/11804192_17.
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 http://dx.doi.org/10.1145/1953122.1953145.
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 http://dx.doi.org/10.1007/978-3-642-14052-5_11.
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 http://dx.doi.org/10.1007/978-3-642-54108-7_10.
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 http://dx.doi.org/10.1007/978-3-642-03359-9_2.
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 http://dx.doi.org/10.1007/s10009-010-0138-x.
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.
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 http://www.spark-2014.org/uploads/erts_2014.pdf.
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 http://dx.doi.org/10.1007/978-3-642-37036-6_8.
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 http://dx.doi.org/10.1007/978-3-642-24690-6_28.
Radu Grigore & MichałMoskal (2007):
Edit and Verify.
In: Workshop on First-Order Theorem Proving (FTP).
Available at http://arxiv.org/abs/0708.0713.
Matt Kaufmann, Panagiotis Manolios & J Strother Moore (2000):
Computer-Aided Reasoning: An Approach.
Kluwer Academic Publishers.
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 http://dx.doi.org/10.3233/978-1-61499-028-4-152.
Summer School Marktoberdorf 2011 lecture notes. A version of this tutorial is available online at http://rise4fun.com/dafny.
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 http://dx.doi.org/10.3233/978-1-58603-976-9-231.
Summer School Marktoberdorf 2008 lecture notes.
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 http://dx.doi.org/10.1007/978-3-642-17511-4_20.
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 http://dx.doi.org/10.1007/978-3-642-27940-9_21.
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 http://research.microsoft.com/pubs/192276/coinduction.pdf.
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 http://dx.doi.org/10.1007/978-3-642-12002-2_26.
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 http://dx.doi.org/10.1007/978-3-540-78800-3_24.
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 http://dx.doi.org/10.1007/3-540-57529-4_61.
Christian Sternagel (2012):
Getting Started with Isabelle/jEdit.
In: Isabelle Users Workshop (IUW).
Available at http://arxiv.org/abs/1208.1368.
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 http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf.