Groups using PVS

From SRI 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 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.
Personal tools