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.
Keywords Formal software verification - Frege Program Prover -
Key system - Perfect developer - Prototype verification system
D. A. Duce, J. Oliveira, P. Boca and R. Boute