MIME-Version: 1.0 Server: CERN/3.0 Date: Tuesday, 07-Jan-97 15:47:18 GMT Content-Type: text/html Content-Length: 5010 Last-Modified: Saturday, 25-May-96 18:48:47 GMT The UV System

The UNITY Verifier System


Attention

There is a new home page for the UV System, Version 2. It is still under construction, but you can already find useful information on this major upgrade.


Introduction

This page describes the UNITY Verifier system (UV system), an interactive symbolic model checker for finite state UNITY programs and propositional UNITY properties.

If you would like to know what model checking for UNITY is all about, you may want to have a look at our brief UV System Introduction.


Documentation

The following documents deal with various aspects of the UV system:

Software Distribution

The current public beta release of the UV system is available as revision 1.20 in two forms:
If you download the system and use it, we would very much like to hear from you. Please send your feedback, bug reports, or suggestions to the author at markus@cs.utexas.edu. Thank you!


Version History

Following is a listing of all distribution releases of the UV system with a short description of changes made at each release:
Revision 1.20 (29-June-1995)
Minor revision, fixed a few bugs in the parser related to type checking and constant folding.
Revision 1.19 (16-March-1995)
Extended the input language by the '%interleaved' directive to specify interleaved BDD indices. Also fixed a bug that caused the parser to complain about conflicting if-cases in assigment statements when there were none. Until an updated version of the language reference manual will be available, you can find more detailed information about the language extension here.
Revision 1.18 (16-February-1995)
Fixed a few problems with the parser (internal memory management and handling of empty sections), and made the program 'View' button of the property info dialog work.
Revision 1.17 (12-January-1995)
Added a missing initialization of the memory statistics routines that could lead to erroneous statistics in the memory dialog, and fixed a bug with the strongest invariant computation that could cause problems in the presence of declared specification variables that were not modified in the program they were declared in.
Revision 1.16 (2-January-1995)
Some minor fixes of interface problems that had gone by unnoticed when we switched from Motif 1.1 to Motif 2.0. The documantation remains unchanged.
Revision 1.14 (18-December-1994)
The initial distribution release.

This page was last updated on 25-May-1996.
Markus Kaltenbach (markus@cs.utexas.edu)