Program Verification with the RISC ProofNavigator
Wolfgang Schreiner · Electronic workshops in computing · 2006
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.