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:
- Model Checking for UNITY,
Technical Report TR94-31, Department of Computer Sciences,
The University of Texas at Austin, December 1994.
The report describes the UV system and the UV input
language. Available are an
abstract, and a compressed
postscript
version of the report.
- The UV System: User Interface Manual
explains how to install and to use the current revision of
the UV system. It is available as a
dvi
version without illustrations, and as a compressed
postscript
version containing a few screen shots of the system interface.
Software Distribution
The current public beta release of the UV system is available as revision
1.20 in two forms:
- the executable archive contains an executable version of the
UV system built for Sun SPARC workstations running SunOS 4.1.3 and the
X Windows System (X11R5).
YOU NEED AN OSF/MOTIF LICENSE FOR ANY COMPUTER YOU WANT TO RUN THIS
SOFTWARE ON.
You can
download
the executable archive.
- the source archive contains the UV system sources needed to
build the UV system. The sources are written entirely in C++ using the
GNU suite of development tools, X Window System Release 5 and OSF/Motif
Version 2.0.
THE SOURCES ARE AVAILABLE UNDER THE GNU PUBLIC LICENSE. YOU NEED THE
X WINDOWS AND MOTIF HEADER FILES AND LIBRARIES INSTALLED ON YOUR COMPUTER
AS WELL AS AN OSF/MOTIF LICENSE TO BE ABLE TO BUILD THE UV SYSTEM.
You can
download
the source archive.
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)