A comparison of tools for teaching formal software verification
Ingo Feinerer, Gernot Salzer · Formal Aspects of Computing · 2008
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.