SRI International Computer Science Laboratory

The PVS Specification and Verification System

 PVS Suggestions

If you have suggestions on how we can improve PVS, we would like to hear from you. Please send suggestions to

Click here for the complete list of suggestions

This list summarizes the suggestions for enhancements that have been received since PVS version 2.2 was announced in September 1998. Most of these were originally sent to Click on the suggestion number for details. The state is one of:

open: The suggestion has been filed
analyzed: We have analyzed the implications of the suggestion, and have made comments
feedback: The suggestion has been implemented, and is being tested
closed: The changes have been integrated in the latest release
suspended: Implementation of the suggestion has been suspended

Note: this makes use of the GNATS bug tracking system available at

No. Status Date Submitted by Synopsis
282feedback1998-10-23Myla Archeruse of labels in "replace" (NRL patches)
284feedback1998-10-29Marcelo GlusmanNames of IMPORTING_TCCs cause loosing proofs
286feedback1998-10-29Ricky ButlerC-u M-x spi suggestion
287feedback1998-11-02Bart Jacobs(UNDO UNDO)
293feedback1998-11-12Arons TamarahTCCs on inst?
296feedback1998-11-16Hendrik Tewsalternate patch files
302open1998-11-23Sam Owrepriority on auto rewrites
303open1998-11-23"Ricky W. Butler"move cursor to current location in Proof buffer
309feedback1998-11-25Hendrik Tews(hide -) does not work
323open1999-01-19John Rushbynormalization in forward chaining and instantiation
347analyzed1999-04-06Hendrik TewsTrapping lisp breaks
349analyzed1999-04-13Paul LoewensteinMore information about TCCs which simplify to FALSE
352open1999-07-11Harald RuessProving Judgement TCCs Suggestion for 3.0
353open1999-08-22Andrew AdamsDependency Analysis Tool Suggestions.
376open1999-11-16Falk BartelsSuggestion: Strategy for case-analysis
384open1999-11-24Marcelo GlusmanBetter proof debugging tools
389open1999-11-24Marcelo Glusmanchoosing values for instantiations
422analyzed2000-01-16Hendrik Tewsdecompose-equality hides sequent
433open2000-02-10John Rushbypermanent log file
536open2001-03-14Hendrik Tewsprojections as functions
537open2001-03-15John Rushbyminor strategy suggestions
581open2001-07-19Tamarah AronsTwo suggestions for enhancements
598open2001-08-07John Rushbysuggestion: print button for sequent displays
599analyzed2001-08-08John Rushbyunname strategy needed
610open2001-09-14Dave Stringer-Calvertinst
630open2001-12-11John Rushbyconversions
692open2002-07-25Hendrik TewsSuggestions for prelude
697open2002-08-01Hendrik Tewsright associative operators
701open2002-08-07Hendrik Tewsfixedpoint lemmas for prelude
702open2002-08-09Hendrik Tewsdocumentation for subtype-tcc and friends

[PVS Home Page]