Worldlex Wiki 
Le Prototype Verification System ( PVS ) est un langage de spécification intégré avec des outils de support et un démonstrateur de théorème automatisé , développé au Computer Science Laboratory de SRI International à Menlo Park, en Californie .
PVS est basé sur un noyau constitué d'une extension de la théorie des types de Church avec des types dépendants , et est fondamentalement une logique d'ordre supérieur typée classique. Les types de base incluent des types non interprétés qui peuvent être introduits par l'utilisateur, et des types intégrés tels que les booléens, les entiers, les réels et les ordinaux. Les constructeurs de types incluent des fonctions, des ensembles, des tuples, des enregistrements, des énumérations et des types de données abstraits. Les sous-types de prédicats et les types dépendants peuvent être utilisés pour introduire des contraintes ; ces types contraints peuvent entraîner des obligations de preuve (appelées conditions de correction de type ou TCC) lors de la vérification de type. Les spécifications PVS sont organisées en théories paramétrées.
Le système est implémenté en Common Lisp et est publié sous la licence publique générale GNU (GPL).