A comparison of tools for teaching formal software verification |
| |
| Authors: | Ingo Feinerer Gernot Salzer |
| |
| Affiliation: | 1. Institut für Computersprachen, Technische Universit?t Wien, Favoritenstr. 9/E185, 1040, Vienna, Austria
|
| |
| 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. |
| |
| Keywords: | Formal software verification Frege Program Prover Key system" target="_blank">Key system Perfect developer Prototype verification system |
| 本文献已被 SpringerLink 等数据库收录！ |
|
