A Specification LanguageTop4 Future WorkReferences

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

A Specification LanguageTop4 Future WorkReferences