References
- [1]
-
Clark Barrett.
CVC Lite Homepage, April 2006.
New York University, NY, http://www.cs.nyu.edu/ acsys/cvcl.
- [2]
-
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.
- [3]
-
Yves Bertot and Pierre Casteran.
Interactive Theorem Proving and Program Development --
Coq'Art: The Calculus of Inductive Constructions.
Texts in Theoretical Computer Science. Springer, Berlin, 2004.
- [4]
-
Bruno Buchberger, Tudor Jebelean, et al.
A Survey of the Theorema project.
In Wolfgang Küchlin, editor, ISSAC'97 International Symposium on
Symbolic and Algebraic Computation, pages 384-391, Maui, Hawaii, July
21-23, 1997. ACM Press, New York.
- [5]
-
S. Buswell and others (eds).
The OpenMath Standard.
Version 2.0, The OpenMath Society, June 2004.
http://www.openmath.org.
- [6]
-
David Carlisle and others (eds).
Mathematical Markup Language (MathML) Version 2.0 (Second Edition).
W3C Recommendation, World Wide Web Consortium, October 2003.
http://www.w3.org/TR/MathML2.
- [7]
-
The Coq Proof Assistant, 2006.
The LogiCal Project, INRIA, France, http://coq.inria.fr.
- [8]
-
C.A.R. Hoare.
An Axiomatic Basis for Computer Programming.
Communications of the ACM, 12(10):576-580, 1969.
- [9]
-
Isabelle, 2006.
University of Cambridge, UK and Technical University Munich, Germany,
http://www.cl.cam.ac.uk/Research/HVG/Isabelle.
- [10]
-
Michael Kohlhase.
OMDoc -- An Open Markup Format for Mathematical Documents (Version
1.2).
Technical Specification and Primer, Saarland University, Germany,
April 2006.
http://www.mathweb.org/omdoc.
- [11]
-
Tobias Nipkow, Lawrence C. Paulson, and Markus Wenzel.
Isabelle/HOL -- A Proof Assistant for Higher-Order Logic,
volume 2283 of Lecture Notes in Computer Science.
Springer, Berlin, 2005.
- [12]
-
S. Owre, J. M. Rushby, and N. Shankar.
PVS: A Prototype Verification System.
In Deepak Kapur, editor, 11th International Conference on
Automated Deduction (CADE), volume 607 of Lecture Notes in Artificial
Intelligence, pages 748-752, Saratoga, NY, June 14-18, 1992. Springer.
- [13]
-
Terence Parr et al.
ANTLR Reference Manual.
Version 2.7.5, University of San Francisco, CA, January 2005.
http://www.antlr.org/doc.
- [14]
-
PVS Specification and Verification System, 2006.
Computer Science Laboratory, Software Research Institute (SRI)
International, Menlo Park, CA, http://pvs.csl.sri.com.
- [15]
-
Wolfgang Schreiner.
Program Verification with the RISC ProofNavigator.
In Teaching Formal Methods: Practice and Experience, BCS-FACS
Christmas Meeting. Electronic Workshops in Computing (eWiC), British
Computer Society, 2006.
- [16]
-
Wolfgang Schreiner.
The RISC ProofNavigator: A Proving Assistant for Program
Verification in the Classroom.
Formal Aspects of Computing, 2007.
To appear.
- [17]
-
SMT-LIB -- The Satisfiability Modulo Theories Library, 2006.
University of Iowa, Iowa City, IA,
http://combination.cs.uiowa.edu/smtlib.
- [18]
-
Overview of Theorema, 2006.
Research Institute for Symbolic Compuation (RISC), Johannes Kepler
University, Linz, Austria, http://www.risc.uni-linz.ac.at/research/theorema.
- [19]
-
Freek Wiedijk, editor.
The Seventeen Provers of the World, volume 3600 of Lecture Notes in Computer Science.
Springer, Berlin, 2006.
Wolfgang
Schreiner