Penelope: an Ada software assurance editor
Carla Marceau, C. Douglas Harper · 2003
The development of a prototype verification editor named Penelope, which allows users to develop specifications, Ada programs, and proofs of verification conditions, is presented. Penelope differs from previous verification systems in that it is interactive, allowing the user to develop specification, program, and proof concurrently. Verification conditions can be inspected and used to guide program development and the correction of errors. The user proves verification conditions within Penelope, appealing to previously formulated axioms and lemmas.>