Groups using PVS

Jump to: navigation, search

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

University of Seville

The following libraries are available at

  • 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.
Personal tools