author = {Wolfgang Schreiner},
title = {{The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom}},
language = {english},
abstract = {This paper gives an overview on the RISC ProofNavigator, an interactive proving assistant for the area of program verification. The assistant combines the user-guided top-down decomposition of proofs with the automatic simplification and closing of proof states by an external satisfiability solver. The software exhibits a modern graphical user interface which has been developed with a focus on simplicity in order to make the software suitable for educational scenarios. Nevertheless, some use cases of a certain level of complexity demonstrate that it may be also appropriate for various realistic applications.},
journal = {Formal Aspects of Computing},
pages = {--},
publisher = {Springer},
address = {London},
isbn_issn = {ISSN 0934-5043},
year = {2008},
month = {April},
note = {The original publication is available at www.springerlink.com. DOI 10.1007/s00165-008-0069-4},
refereed = {yes},
keywords = {Interactive Proving Assistants, Computer-Aided Verification, Teaching Formal Methods.},
length = {15},
url = {http://dx.doi.org/10.1007/s00165-008-0069-4}