Towards a Customizable PVS

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 customization 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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Jan 01, 2000
Accession Number
ADA373581

Entities

People

  • Ben Divito
  • Cesar Munoz
  • Gerald Luttgen
  • Paul Miner
  • Ricky Butler

Tags

Communities of Interest

  • Materials and Manufacturing Processes

DTIC Thesaurus Topics

  • Case Studies
  • Coding
  • Cognitive Systems Engineering
  • Computer Programming
  • Computer Science
  • Computers
  • Electronic Mail
  • Engineering
  • Engineers
  • Language
  • Lisp Programming Language
  • Notation
  • Programming Languages
  • Propulsion Systems
  • Recursive Functions
  • Software Development
  • Specifications

Fields of Study

  • Computer science

Readers

  • Mathematical Modeling and Probability Theory.
  • Software Engineering.
  • Technical Research and Report Writing.