A comparison of tools for teaching formal software verification

DOI10.1007/S00165-008-0084-5MaRDI QIDQ1019026zbMATH OpenOpenAlexWikidataFDO

Authors Ingo Feinerer, Gernot Salzer

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-0084-5

zbMATH Keywords

prototype verification systemformal software verificationFrege Program ProverKey systemperfect developer

Mathematics Subject Classification ID

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

Recommendations

• Verified squared, does critical software deserve verified tools?
• Software Verification and Analysis
• The RISC ProofNavigator: a proving assistant for program verification in the classroom
• A verification tool developer's vade mecum.
• Mathematics and Software Verification

Cited in

(2)

• Applying formal concepts to learning systems validation
• A verification tool developer's vade mecum.

Describes a project that uses

Uses Software

• Analytica
• KeY
• PVS

This page was built for publication: A comparison of tools for teaching formal software verification

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1019026)