PVS为在计算机科学中严格、高效地应用形式化方法提供自动化的机器支持,它易于安装、使用和维护,足一个良好的集成环境.该系统主要包括规约语言和定理证明器两部分,并且还集成了解释器、类型检查器及预定义的规约库和各种方便的浏览、编辑工具.PvS提供的规约语言基于高阶逻拜,具有丰富的类型系统,是一般适用的语言,表达能力很强,大多数数学概念、计算概念均可用该语言自然直接地表示出来.PVS的定理证明器以交互方式工作,同时又具备高度的自动化水准.它的命令的能力很强,琐屑的证明细节为证明器的内部推理机制掩盖,使得用户仅在关健决策点上控制证明过程.