Wolfgang Schreiner,
"The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom"
, in Formal Aspects of Computing, Springer, 4-2008, ISSN: 0934-5043
Original Titel:
The RISC ProofNavigator: A Proving Assistant for Program Verification in the Classroom
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Journal:
Formal Aspects of Computing
Veröffentlicher:
Springer
Erscheinungsmonat:
4
Erscheinungsjahr:
2008
ISSN:
0934-5043
Anzahl der Seiten:
15
Notiz zur Publikation:
The original publication is available at www.springerlink.com. DOI 10.1007/s00165-008-0069-4