Groups using PVS
NASA Langley is one of our sponsors and has many PVS users. They have an extensive set of libraries and extensions available at http://shemesh.larc.nasa.gov/fm/fm-pvs.html
University of Seville
The following libraries are available at http://www.glc.us.es/wiki/Theories#Theories_in_PVS
- A Formalization of Abstract Properties of Confluent Reductions in PVS.
- Proving termination with multiset orderings in PVS: theory, methodology and applications (PROTEMO).
- A formally verified prover for the ALC description logic (in PVS).
- Verification of the formal concept analysis in PVS.
- A formally verified proof in PVS of the strong completeness theorem of propositional SLD-resolution.
- Theory of Refinements in PVS.