The UNITY Verifier System (Version 2)
Warning
The pages describing the various aspects of the UNITY Verifier System
(Version 2) are currently under construction and might be updated
without prior notice.
Information about the UV System (Current Version: 2.3.3)
The following pages contain information about different aspects of the
UV system. Much of the online documentation is still under development
and will be updated continually.
- The what is new page will keep you informed about
recent changes and improvements to the UV system. Since both the system
and its documentation are in the early stages of an alpha release, it is
a good idea to check often what is happening.
- A very brief introduction to the UV system
will help you with getting started to learn what model checking for
UNITY is about.
- An online manual is available to answer
your questions about the structure, the operation and the user interface
of the UV system.
- Local access information is provided to help
you with running the UV system on computers of the UT CS department.
- If you have used version 1 of the UV system before, you might find a
brief summary of the main differences between
versions 1 and 2 interesting.
- You can also access the home page for the
UV System (Version 1). Note, however, that version 1 is to be
replaced by version 2 and won't be supported any longer.
Introduction
Welcome to the UNITY Verifier system (UV system),
an interactive symbolic model checker for finite state UNITY programs
and propositional UNITY logic.
The UV system was first released publically at the end of 1994 with the
goals of providing a useful tool for designing and verifying UNITY
programs, and of serving as an experimental platform for reseach in
automated and interactive verification of concurrent systems.
Based on the experience gained with the initial version of the UV
system we set out to improve the system in several ways, including
with respect to its overall structure, the expressiveness of the UV
input language, and the design of its user interface.
The process of modification and extension is not yet completed, but we
are now ready to announce the first alpha release of the redesigned UV
system, referred to as version 2.
Although work continues on several of the modifications and
extensions, we would like to invite you to have a look at version 2
and let us know what you think about it.
Feedback Welcome
We love to hear from you! No matter whether you discover bugs, have
suggestions or comments, or would like to tell us about how you can
(or cannot) use the UV system for your work, all forms of feedback are
welcome.
You can send mail to Markus Kaltenbach at markus@cs.utexas.edu with your
questions, suggesions, or complaints.
This page was last updated on 13-June-1996.
markus@cs.utexas.edu