The RISC ProofNavigator: a proving assistant for program verification in the classroom

DOI10.1007/s00165-008-0069-4zbMath1162.68478OpenAlexW2007452988MaRDI QIDQ1019024

Wolfgang Schreiner

Publication date: 27 May 2009

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-008-0069-4

zbMATH Keywords

computer-aided verificationinteractive proving assistantsteaching formal methods

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Uses Software

• Coq
• Theorema
• PVS
• OMDoc
• CVC Lite

Cites Work

• Unnamed Item
• \textit{Theorema}: Towards computer-aided mathematical theory exploration
• Isabelle/HOL. A proof assistant for higher-order logic
• Click’n Prove: Interactive Proofs within Set Theory
• Logic in Computer Science
• Computer Aided Verification
• An axiomatic basis for computer programming

This page was built for publication: The RISC ProofNavigator: a proving assistant for program verification in the classroom