Practicals

Practicals is a package for programming strategies in PVS with high level tacticals. Practicals enhances the PVS proof language (IF, REPEAT, THEN, TRY, ...) with tacticals for

• Looping (WHILE, FOR)
• Matching terms (MATCH)
• Matching proof contexts (SCREEN)
• Raising proof failures (THROW)
• Catching proof failures (CATCH), and more ...

Practicals was developed by Florent Kirchner while in residence in the Formal Methods group at the National Institute of Aerospace (NIA).

• README.
• Practicals Package (lisp file).
• Documentation (ps, pdf).

Publications

• Florent Kirchner and César Muñoz, The Proof Monad, Journal of Logic and Algebraic Programming, Volume 79, Issues 3-5, pp. 264-277, April-July 2010. BibTeX Reference.
• Florent Kirchner and César Muñoz, PVS#: Streamlined Tacticals for PVS, Electronic Notes in Theoretical Computer Science, Volume 174, Issue 11, July 2007. BibTeX Reference.

Note: The tag identifies links that are outside of the NASA domain.