Operated by Universities Space Research Association DISTRIBUTION STATEMENT A Approved for Public Release Distribution Unlimited

Abstract. PVS is a state-of-the-art theorem-proving tool developed by SRI International. It is used in a variety of academic and real-world applications by NASA and ICASE researchers, for whom tool cus-tomization and extensibility are becoming increasingly important issues. This paper shows, by referring to past experiences with several projects and case studies, that the customization features currently offered by PVS are often insufficient. It also suggests several improvements regarding PVS's customization in the short run and regarding its extensibility in the long run