References

[1]   ANTLR v3 Parser Generator, 2010. http://www.antlr.org.

[2]   Clark Barrett. CVC Lite Homepage, April 2006. New York University, NY, http://www.cs.nyu.edu/acsys/cvcl.

[3]   Clark Barrett and Sergey Berezin. 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, volume 3114 of Lecture Notes in Computer Science, pages 515–518. Springer, 2004.

[4]   The Java Modeling Language (JML), 2010. http://www.jmlspecs.org.

[5]   The RISC ProofNavigator, 2010. Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, http://www.risc.jku.at/research/formal/software/ProofNavigator.

[6]   Wolfgang Schreiner. A Program Calculus. Technical report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, September 2008. http://www.risc.jku.at/people/schreine/papers/ProgramCalculus2008.pdf.

[7]   Wolfgang Schreiner. Understanding Programs. Technical report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, July 2008. http://www.risc.uni-linz.ac.at/people/schreine/papers/Understanding2008.pdf.

[8]   Wolfgang Schreiner. The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom. Formal Aspects of Computing, 21(3):277–291, 2009.

[9]   Wolfgang Schreiner. Computer-Assisted Program Reasoning Based on a Relational Semantics of Programs. In Pedro Quaresma and Ralph-Johan Back, editors, THedu’11, CTP Components for Educational Software, Workshop associated to CADE-23, Wroclaw, Poland, July 31, 2011, number 79 in Electronic Proceedings in Theoretical Computer Science (EPTCS), pages 124–142, February 2012. http://dx.doi.org/10.4204/EPTCS.79.8.