References

  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 http://dx.doi.org/10.1007/11804192_17.
  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 http://dx.doi.org/10.1145/1953122.1953145.
  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 http://dx.doi.org/10.1007/978-3-642-14052-5_11.
  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 http://dx.doi.org/10.1007/978-3-642-54108-7_10.
  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 http://dx.doi.org/10.1007/978-3-642-03359-9_2.
  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 http://dx.doi.org/10.1007/s10009-010-0138-x.
  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 http://www.spark-2014.org/uploads/erts_2014.pdf.
  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 http://dx.doi.org/10.1007/978-3-642-37036-6_8.
  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 http://dx.doi.org/10.1007/978-3-642-24690-6_28.
  11. Radu Grigore & MichałMoskal (2007): Edit and Verify. In: Workshop on First-Order Theorem Proving (FTP). Available at http://arxiv.org/abs/0708.0713.
  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 http://formal.iti.kit.edu/~klebanov/pubs/thesis-klebanov.pdf.
  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 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.
  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 http://dx.doi.org/10.3233/978-1-58603-976-9-231. 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 http://dx.doi.org/10.1007/978-3-642-17511-4_20.
  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 http://dx.doi.org/10.1007/978-3-642-27940-9_21.
  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 http://research.microsoft.com/pubs/192276/coinduction.pdf.
  19. K. Rustan M. Leino, MichałMoskal & Wolfram Schulte (2008): Verification Condition Splitting. Technical Report. Microsoft Research. Available at http://research.microsoft.com/pubs/77373/VerificationConditionSplitting(Draft2008).pdf. 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 http://dx.doi.org/10.1007/978-3-642-12002-2_26.
  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 http://dx.doi.org/10.1007/978-3-540-78800-3_24.
  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 http://dx.doi.org/10.1007/3-540-57529-4_61.
  23. Christian Sternagel (2012): Getting Started with Isabelle/jEdit. In: Isabelle Users Workshop (IUW). Available at http://arxiv.org/abs/1208.1368.
  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 http://www4.in.tum.de/~wenzelm/papers/async-isabelle-scala.pdf.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org