References

1. Mike Barnett, Manuel Fähndrich, K. Rustan M. Leino, Peter Müller, Wolfram Schulte & Herman Venter (2011): Specification and verification: the Spec# experience. Commun. ACM 54(6), pp. 81–91, doi:10.1145/1953122.1953145. http://specsharp.codeplex.com/.
2. Daniel Bruns (2011): Specification of Red-black Trees: Showcasing Dynamic Frames, Model Fields and Sequences. In: 10th KeY Symposium. http://digbib.ubka.uni-karlsruhe.de/volltexte/1000024828.
3. Ernie Cohen, Markus Dahlweid, Mark A. Hillebrand, Dirk Leinenbach, Michal Moskal, Thomas Santen, Wolfram Schulte & Stephan Tobies (2009): VCC: A Practical System for Verifying Concurrent C. In: TPHOLs, LNCS 5674. Springer, pp. 23–42, doi:10.1007/978-3-642-03359-9_2. http://vcc.codeplex.com/.
4. (Last access: Nov. 2014): Dafny example gallery. http://dafny.codeplex.com/SourceControl/latest.
5. C. Neville Dean & Raymond T. Boute (2004): Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18–19, 2004, Proceedings. LNCS 3294. Springer, doi:10.1007/b102075.
6. Jeremy Gibbons & José Nuno Oliveira (2009): Teaching Formal Methods, Second International Conference, TFM 2009, Eindhoven, The Netherlands, November 2–6, 2009. Proceedings. LNCS 5846. Springer, doi:10.1007/978-3-642-04912-5.
7. Christoph Gladisch & Shmuel Tyszberowicz (2013): Specifying a Linked Data Structure in JML for Formal Verification and Runtime Checking. In: SBMF, LNCS 8195. Springer, pp. 99–114, doi:10.1007/978-3-642-41071-0_8.
8. Z. Istenes (2008): Formal Methods in Computer Science Education, FORMED 2008, Budapest, Hungary, March 29, 2008, Proceedings. http://157.181.166.108/pdf/FORMED_2008.pdf.
9. Mathieu Jaume & Théo Laurent (2014): Teaching Formal Methods and Discrete Mathematics. In: F-IDE, EPTCS 149, pp. 30–43, doi:10.4204/EPTCS.149.4.
10. Joseph R. Kiniry & Daniel M. Zimmerman (2008): Secret Ninja Formal Methods. In: FM 2008, LNCS 5014. Springer, pp. 214–228, doi:10.1007/978-3-540-68237-0_16.
11. K. Rustan M. Leino (2008): This is Boogie 2. Technical Report. Microsoft Research. Available at http://research.microsoft.com/apps/pubs/default.aspx?id=147643. http://research.microsoft.com/apps/pubs/default.aspx?id=147643.
12. K. Rustan M. Leino (2010): Dafny: An Automatic Program Verifier for Functional Correctness. In: LPAR-16, LNCS 6355. Springer, pp. 348–370, doi:10.1007/978-3-642-17511-4_20. http://research.microsoft.com/en-us/projects/dafny/.
13. K. Rustan M. Leino & MichałMoskal (2010): Usable Auto-Active Verification. In: Usable Verification Workshop. http://fm.csl.sri.com/UV10/.
14. K. Rustan M. Leino & Peter Müller (2004): Object Invariants in Dynamic Contexts. In: ECOOP, LNCS 3086. Springer, pp. 491–516, doi:10.1007/978-3-540-24851-4_22.
15. Hannes Mehnert, Filip Sieczkowski, Lars Birkedal & Peter Sestoft (2012): Formalized Verification of Snapshotable Trees: Separation and Sharing. In: VSTTE, LNCS 7152, pp. 179–195, doi:10.1007/978-3-642-27705-4_15.
16. Stefan Mitsch, Jan-David Quesel & André Platzer (2014): Refactoring, Refinement, and Reasoning – A Logical Characterization for Hybrid Systems. In: FM, LNCS 8442. Springer, pp. 481–496, doi:10.1007/978-3-319-06410-9_33.
17. Nadia Polikarpova, Carlo A. Furia & Bertrand Meyer (2010): Specifying Reusable Components. In: VSTTE, LNCS 6217. Springer, pp. 127–141, doi:10.1007/978-3-642-15057-9_9.
18. Nadia Polikarpova, Julian Tschannen & Carlo A. Furia (2015): A Fully Verified Container Library. In: FM, LNCS 9109. Springer, pp. 414–434, doi:10.1007/978-3-319-19249-9_26.
19. Nadia Polikarpova, Julian Tschannen, Carlo A. Furia & Bertrand Meyer (2014): Flexible Invariants Through Semantic Collaboration. In: FM, LNCS 8442. Springer, pp. 514–530, doi:10.1007/978-3-319-06410-9_35.
20. Erik Poll (2009): Teaching Program Specification and Verification Using JML and ESC/Java2. In: TFM 2009, LNCS 5846. Springer, pp. 92–104, doi:10.1007/978-3-642-04912-5_7.
21. Julian Tschannen, Carlo A. Furia & Martin Nordio (2014): AutoProof Meets Some Verification Challenges. International Journal on Software Tools for Technology Transfer, doi:10.1007/s10009-014-0300-y.
22. Julian Tschannen, Carlo A. Furia, Martin Nordio & Bertrand Meyer (2011): Usable Verification of Object-Oriented Programs by Combining Static and Dynamic Techniques. In: SEFM, LNCS 7041. Springer, pp. 382–398, doi:10.1007/978-3-642-24690-6_26.
23. Julian Tschannen, Carlo A. Furia, Martin Nordio & Nadia Polikarpova (2015): AutoProof: Auto-active Functional Verification of Object-oriented Programs. In: TACAS, LNCS 9035. Springer, pp. 566–580, doi:10.1007/978-3-662-46681-0_53.
24. (Last access: Nov. 2014): VeriFast example gallery. http://people.cs.kuleuven.be/~bart.jacobs/verifast/examples/.
25. (Last access: Nov. 2014): Why3 example gallery. http://toccata.lri.fr/gallery/why3.en.html.

Comments and questions to: eptcs@eptcs.org

For website issues: webmaster@eptcs.org