×

The RISC ProofNavigator: a proving assistant for program verification in the classroom. (English) Zbl 1162.68478

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)

Software:

Theorema; PVS; Coq; OMDoc; CVC Lite
PDFBibTeX XMLCite
Full Text: DOI HAL

References:

[1] Aspinall D et al (eds) User interfaces for theorem provers, satellite workshop of ETAPS 2005, Edinburgh, UK, 9 April 2005. http://homepages.inf.ed.ac.uk/da/uitp05
[2] Abrial J-R, Cansell D (2003) Click’n prove: interactive proofs within set theory. In: Basin DA, Wolff B(eds) TPHOLs 2003, vol 2758 of LNCS. Springer, Heidelberg, pp 1–24 · Zbl 1279.68283
[3] Barrett C, Berezin S (2004) CVC Lite: a new implementation of the cooperating validity checker. In: Computer aided verification: 16th international conference, CAV 2004, Boston, MA, USA, 13–17 July 2004, vol 3114 of LNCS, pp 515–518. Springer, Heidelberg · Zbl 1103.68605
[4] Bertot Y, Casteran P (2004) Interactive theorem proving and program development–Coq’Art: the calculus of inductive constructions. Texts in theoretical computer science. Springer, Berlin
[5] Buchberger B, Craciun A, Jebelean T et al (2006) Theorema: towards computer-aided mathematical theory exploration. J Appl Logic 4(4): 470–504 · Zbl 1107.68095 · doi:10.1016/j.jal.2005.10.006
[6] Beckert, B, Hähnle, R, Schmitt, PH (eds) (2007) Verification of object-oriented software: the KeY Approach. Springer, Heidelberg
[7] Buswell S, others (eds) (2004) The OpenMath standard. Version 2.0, The OpenMath Society, June 2004. http://www.openmath.org
[8] Carter G, Monahan R, Morris JM (2005) Software refinement with perfect developer. In: SEFM’05: 3rd IEEE international conference on software engineering and formal methods, pp 363–373, Koblenz, Germany, IEEE Computer Society, 5–9 September 2005
[9] Feinerer I (2005) Formal program verification: a comparison of selected tools and their theoretical foundations. Master’s Thesis, Theory and Logic Group, Institute of Computer Languages, Vienna University of Technology, Vienna, Austria
[10] Formal Methods for Software Development (2007) 6 ECTS credits course, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. http://www.risc.uni-linz.ac.at/people/schreine/courses/ss2007/formal
[11] Gallier JH (1986) Logic for computer science–foundations of automatic theorem proving. Harper & Row, New York · Zbl 0605.03004
[12] Hoare CAR (1969) An axiomatic basis for computer programming. Commun ACM 12(10): 576–580 · Zbl 0179.23105 · doi:10.1145/363235.363259
[13] Huth M, Ryan M (2004) Logic in computer science–modelling and reasoning about systems, 2nd edn. Cambridge University Press, Cambridge · Zbl 1073.68001
[14] Kaufmann M, Manolios P, Strother Moore J (2000) Computer-aided reasoning: an approach. Kluwer, Dordrecht
[15] Kohlhase M (2006) OMDoc–an open markup format for mathematical documents (version 1.2). Technical specification and primer, Saarland University, Germany. http://www.mathweb.org/omdoc
[16] Nipkow T, Paulson LC, Wenzel M (2005) Isabelle/HOL–a proof assistant for higher-order logic, vol 2283 of Lecture Notes in Computer Science. Springer, Berlin · Zbl 0994.68131
[17] Owre S, Rushby JM, Shankar N (1992) PVS: a prototype verification system. In: Kapur D (ed) 11th international conference on automated deduction (CADE), vol 607 of Lecture Notes in Artificial Intelligence, pp 748–752, Saratoga, 14–18 June 1992. Springer, Heidelberg
[18] Reasoning about Programs (2007) Course at the school of computing and mathematical sciences, University of Waikato, New Zealand, http://www.cs.waikato.ac.nz/\(\sim\)robi/comp340-07b/
[19] The RISC ProofNavigator (2006) Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria. http://www.risc.uni-linz.ac.at/research/formal/software/ProofNavigator
[20] Schreiner W (2006) Program verification with the RISC ProofNavigator. In: Teaching formal methods: practice and experience, electronic workshops in computing (eWiC), BCS-FACS Christmas Meeting, London, UK, December 15. British Computer Society
[21] Schreiner W (2006) The RISC ProofNavigator–tutorial and manual. Technical report, Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria
[22] SMT-LIB–the satisfiability modulo theories library (2006) University of Iowa, Iowa City, IA. http://combination.cs.uiowa.edu/smtlib
[23] Wiedijk, F (eds) (2006) The seventeen provers of the world, vol 3600 of Lecture Notes in Computer Science. Springer, Berlin
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.