The current release is UCLID version 3.1.
The easiest way to try out UCLID is by downloading the following VM image, which has UCLID pre-installed.
You can also download UCLID as VirtualBox virtual machine (VM) image.
This Fedora 6 VM has the latest UCLID binaries and the Minisat solver installed and ready to use.
We also have a bytecode distribution, containing documentation, examples, and bytecode. Currently version 3.1 is only available for Linux on x86 architectures (both 32 and 64 bit). Installation instructions are in the README file. Version 3.1 uses Ofer Strichman's psep library (but you do not need to separately download and install it).
UCLID is largely implemented in Moscow ML. To use UCLID, you will also need to download and install the following support software before installing UCLID:
UCLID is released under the BSD license. See the "LICENSE" file included in the distribution.
Download the user manual in PDF.
If you download and use UCLID, please let us know by e-mailing Sanjit Seshia or Rohit Sinha (for e-mail addresses, see here).
Here is a UCLID model of CloudProxy as described in our VSTTE'14 paper. This model makes heavy use of terms and uninterpreted functions.
Here are some UCLID models (e.g. Bochs Translation Lookaside Buffer module, SecVisor) described in our FMCAD'12 and MEMOCODE'13 papers. These models make heavy use of bit-vectors.
Some other examples from Computer Security:
Here are some examples of purely term-level UCLID specifications that are mentioned in our CAV'02 and FMCAD'02 papers:
For other examples, including bit-vector examples, look in the tarfile.
Scores of benchmark SMT formulas have been generated using UCLID, and these have all been contributed to SMTLIB.
For historical reference, here are tarred-gzipped files containing some of the original benchmark formulas generated using UCLID, in different formats (as given below):