"Program Verification with the RISC ProofNavigator"
, in David Duce and Paul Boca: Proceedings of: Teaching Formal Methods: Practice and Experience (at BCS-FACS Christmas Meeting), Serie Electronic Workshops in Computing (eWiC), British Computer Society, London, UK, Seite(n) 1--6, 2006
Program Verification with the RISC ProofNavigator
Sprache des Titels:
Proceedings of: Teaching Formal Methods: Practice and Experience (at BCS-FACS Christmas Meeting)
This paper describes the use of the RISC ProofNavigator, an interactive proving assistant for the area of program verification. This assistant has been developed with a focus on simplicity and ease of use; it is intended to be suitable for educational scenarios as well as for realistic applications.