Program Verification with the RISC ProofNavigator

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.

Content

Author and article information

Contributors

Wolfgang Schreiner

Conference

Publication date: December 2006

Publication date (Print): December 2006

Pages: 1-6

Affiliations

[0001]Research Institute for Symbolic Computation (RISC)

Johannes Kepler University, Linz, Austria

http://www.risc.uni-linz.ac.at

Article

DOI: 10.14236/ewic/TFM2006.3

SO-VID: 711b061b-cc8c-4f02-9b35-d98e663d6113

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Teaching Formal Methods: Practice and Experience

Conference acronym: TFM

Conference number:

Conference location: BCS London Office, UK

Conference date: 15 December 2006

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Teaching Formal Methods: Practice and Experience

History

Product

1477-9358 BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/TFM2006.3

Self URI (journal page): https://ewic.bcs.org/

Celebrating 65 years of The Computer Journal - free-to-read perspectives - bcs.org/tcj65

Program Verification with the RISC ProofNavigator

Abstract