References

  1. R.-J. Back & J. von Wright (1998): Refinement Calculus: A Systematic Introduction. Springer, New York.
  2. Ralph-Johan Back (2009): Invariant Based Programming: Basic Approach and Teaching Experiences. Formal Aspects of Computing 21(3), pp. 227–244, doi:10.1007/s00165-008-0070-y.
  3. Clark Barrett & Sergey Berezin (2004): CVC Lite: A New Implementation of the Cooperating Validity Checker. In: Computer Aided Verification: 16th International Conference, CAV 2004, Boston, MA, USA, July 13–17, 2004, LNCS 3114. Springer, pp. 515–518, doi:10.1007/978-3-540-27813-9_49.
  4. Bernhard Beckert, Reiner Hähnle & Peter H. Schmitt (2007): Verification of Object-Oriented Software: The KeY Approach. LNCS 4334. Springer, doi:10.1007/978-3-540-69061-0.
  5. P. Boca, J. P. Bowen & D. A. Duce (2006): Teaching Formal Methods: Practice and Experience. Electronic Workshops in Computing (eWIC). British Computer Society, London, UK, December 16. http://www.bcs.org/category/8726.
  6. Raymond T. Boute (2006): Calculational Semantics: Deriving Programming Theories from Equations by Functional Predicate Calculus. ACM Transactions on Programming Languages and Systems 28(4), pp. 747–793, doi:10.1145/1146809.1146814.
  7. Lilian Burdy, Yoonsik Cheon, David R. Cok, Michael D. Ernst, Joseph R. Kiniry, Gary T. Leavens, K. Rustan M. Leino & Erik Poll (2005): An Overview of JML Tools and Applications. International Journal on Software Tools for Technology Transfer 7, pp. 212–232, doi:10.1007/s10009-004-0167-4.
  8. C. Neville Dean & Raymond T. Boute (2004): Teaching Formal Methods, CoLogNET/FME Symposium, TFM 2004, Ghent, Belgium, November 18–19, 2004. LNCS 3294. Springer, doi:10.1007/b102075.
  9. Edsger W. Dijkstra (1968): A Constructive Approach to the Problem of Program Correctness. BIT Numerical Mathematics 8(3), pp. 174–186, doi:10.1007/BF01933419.
  10. Ingo Feinerer & Gernot Salzer (2009): A Comparison of Tools for Teaching Formal Software Verification. Formal Aspects of Computing 21(3), pp. 293–301, doi:10.1007/s00165-008-0084-5.
  11. Jean-Christophe Filliâtre & Claude Marché (2007): The Why/Krakatoa/Caduceus Platform for Deductive Program Verification. In: Computer Aided Verification, 19th International Conference, CAV 2007, Berlin, Germany, July 3-7, 2007, LNCS 4590. Springer, pp. 173–177, doi:10.1007/978-3-540-73368-3_21.
  12. Jeremy Gibbons & José Nuno Oliveira (2009): Teaching Formal Methods, Second International Conference, TFM 2009, Eindhoven, The Netherlands, November 2–6, 2009. Lecture Notes in Computer Science 5846. Springer, doi:10.1007/978-3-642-04912-5.
  13. Mike Gordon (2010): Specification and Verification I. University of Cambridge, UK, Lecture Notes, http://www.cl.cam.ac.uk/~mjcg/Lectures/SpecVer1/SpecVer1.html.
  14. Eric C.R. Hehner (2006): A Practical Theory of Programming. Springer, New York. http://www.cs.utoronto.ca/~hehner/aPToP.
  15. C.A.R. Hoare & He Jifeng (1998): Unifying Theories of Programming. Prentice Hall, London, UK. Available at http://www.unifyingtheories.org.
  16. Leslie Lamport (2002): Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley. Available at http://research.microsoft.com/users/lamport/tla/book.html.
  17. Carroll Morgan (1998): Programming from Specifications, 2nd edition. Prentice Hall, London, UK. Available at http://www.cs.ox.ac.uk/publications/books/PfS.
  18. J. M. Morris (1987): A Theoretical Basis for Stepwise Refinement and the Programming Calculus. Science of Computer Programming 9(3), pp. 287–306, doi:10.1016/0167-6423(87)90011-6.
  19. José Nuno Oliveira (2004): A Survey of Formal Methods Courses in European Higher Education. In: TFM2004, pp. 235–248, doi:10.1007/978-3-540-30472-2_16.
  20. S. Owre, J. M. Rushby & N. Shankar (1992): PVS: A Prototype Verification System. In: Deepak Kapur: 11th International Conference on Automated Deduction (CADE), Lecture Notes in Artificial Intelligence 607. Springer, Saratoga, NY, June 14–18, pp. 748–752, doi:10.1007/3-540-55602-8_217.
  21. David A. Schmidt (1986): Denotational Semantics – A Methodology for Language Development. Allyn and Bacon, Boston, MA. Available at http://people.cis.ksu.edu/~schmidt/text/densem.html.
  22. Wolfgang Schreiner (2008): A Program Calculus. Technical Report. RISC, Johannes Kepler University, Linz, Austria. http://www.risc.jku.at/people/schreine/papers/ProgramCalculus2008.pdf.
  23. Wolfgang Schreiner (2008): Understanding Programs. Technical Report. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. http://www.risc.uni-linz.ac.at/people/schreine/papers/Understanding2008.pdf.
  24. Wolfgang Schreiner (2009): The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom. Formal Aspects of Computing 21(3), pp. 277–291, doi:10.1007/s00165-008-0069-4.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org