The PVS Specification and Verification System

If you have suggestions on how we can improve PVS, we would like to hear from you. Please send suggestions to pvs-bugs@csl.sri.com.

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 pvs-bugs@csl.sri.com. 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 ftp://prep.ai.mit.edu/pub/gnu/.

No.	Status	Date	Submitted by	Synopsis
282	feedback	1998-10-23	Myla Archer	use of labels in "replace" (NRL patches)
284	feedback	1998-10-29	Marcelo Glusman	Names of IMPORTING_TCCs cause loosing proofs
286	feedback	1998-10-29	Ricky Butler	C-u M-x spi suggestion
287	feedback	1998-11-02	Bart Jacobs	(UNDO UNDO)
293	feedback	1998-11-12	Arons Tamarah	TCCs on inst?
296	feedback	1998-11-16	Hendrik Tews	alternate patch files
302	open	1998-11-23	Sam Owre	priority on auto rewrites
303	open	1998-11-23	"Ricky W. Butler"	move cursor to current location in Proof buffer
309	feedback	1998-11-25	Hendrik Tews	(hide -) does not work
323	open	1999-01-19	John Rushby	normalization in forward chaining and instantiation
347	analyzed	1999-04-06	Hendrik Tews	Trapping lisp breaks
349	analyzed	1999-04-13	Paul Loewenstein	More information about TCCs which simplify to FALSE
352	open	1999-07-11	Harald Ruess	Proving Judgement TCCs Suggestion for 3.0
353	open	1999-08-22	Andrew Adams	Dependency Analysis Tool Suggestions.
376	open	1999-11-16	Falk Bartels	Suggestion: Strategy for case-analysis
384	open	1999-11-24	Marcelo Glusman	Better proof debugging tools
389	open	1999-11-24	Marcelo Glusman	choosing values for instantiations
422	analyzed	2000-01-16	Hendrik Tews	decompose-equality hides sequent
433	open	2000-02-10	John Rushby	permanent log file
536	open	2001-03-14	Hendrik Tews	projections as functions
537	open	2001-03-15	John Rushby	minor strategy suggestions
581	open	2001-07-19	Tamarah Arons	Two suggestions for enhancements
598	open	2001-08-07	John Rushby	suggestion: print button for sequent displays
599	analyzed	2001-08-08	John Rushby	unname strategy needed
610	open	2001-09-14	Dave Stringer-Calvert	inst
630	open	2001-12-11	John Rushby	conversions
692	open	2002-07-25	Hendrik Tews	Suggestions for prelude
697	open	2002-08-01	Hendrik Tews	right associative operators
701	open	2002-08-07	Hendrik Tews	fixedpoint lemmas for prelude
702	open	2002-08-09	Hendrik Tews	documentation for subtype-tcc and friends

[PVS Home Page]