# Groups using PVS

From SRI PVS

## NASA Langley

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.