Journal ArticleOPEN ACCESS

A comparison of tools for teaching formal software verification

Formal Aspects of Computing (2009) 21(3) 293-301
DOI: 10.1007/s00165-008-0084-5
7Citations
Citations of this article
11Readers
Mendeley users who have this article in their library.

Abstract

We compare four tools regarding their suitability for teaching formal software verification, namely the Frege Program Prover, the Key system, Perfect Developer, and the Prototype Verification System (PVS). We evaluate them on a suite of small programs, which are typical of courses dealing with Hoare-style verification, weakest preconditions, or dynamic logic. Finally we report our experiences with using Perfect Developer in class. © 2008 British Computer Society.

Author supplied keywords

Cite

CITATION STYLE

APA

Feinerer, I., & Salzer, G. (2009). A comparison of tools for teaching formal software verification. Formal Aspects of Computing, 21(3), 293–301. https://doi.org/10.1007/s00165-008-0084-5

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free