2008/06/10 by Ingo Feinerer, Gernot Salzer · 1 citation
Computer Science · #Logic, programming, and type systems #Software Engineering Research #Software Testing and Debugging Techniques
paper · pdf · doi:10.1007/s00165-008-0084-5
openalex publication_date 2008/06/10 · openalex created_date 2016/06/24 · openalex updated_date 2026/07/23
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.