PVS是原型验证系统(Prototype Verification System)的缩写，斯坦福研究机构在过去20年中开发了一系列验证系统。开发PVS的目的是把它作为一个重量级验证系统EHDM的轻量级原型，以探索实现EHDM所需的相关技术，PVS这一名字正是由此而来.我们在设计并发面向对象广谱规约语言ND一C00SL时，拟对该语言的核心部分进行验证，因此，对PVS作了较为深入的剖析。
