RISC RISC Research Institute for Symbolic Computation  
  • @article{RISC3411,
    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}