Analysis of Theorem-proving Aiding Tool──PVS
Dajun Yang · Jisuanji gongcheng · 2000
PVS is a powerful specification and verification system developed by Stanford Research Inshtute, its application area is broad. After briefly introducing the composition and function of PVS, this paper puts great emphasis on analyzing the features of PVS'specification language, verification system and design decisions, as well as inner mechanisms that make PVS powerful and flexible.