Releases: uclid-org/uclid
Releases · uclid-org/uclid
Tag before removing horn solver
This tag is the last tag before the horn solver and lazy SC solver are removed.
May 2020 Release
From a user perspective, this release contains some bug fixes and a new synthesis interface.
From a developer perspective, this tag marks a significant change in the git history.
Yet another release
This release
uclid-0.9.5.zip
contains a few more bugfixes.
UCLID5 v0.9.5b New Public Release
Main new feature in this release is hyperproperty verification using BMC. See test/test-hyperproperty-*.ucl for examples.
We have also added support for quantifier patterns. See examples/hash.ucl for an example.
Several bugs have been fixed.
We have experimental support for unbounded model checking using the Z3/SPACER. Documentation for this feature will be added when this feature becomes more stable.
uclid5 v0.9.5 alpha release
What's new?
- Much improved tutorial.
- Initial support for SyGuS
- New operators (distinct, bv_sign_extend, bv_zero_extend).
- Local scoped variables are allowed in every block now.
- We have the beginnings of an optimizer.
- Lots and lots and lots of bugfixes.
uclid5 v0.9.1 alpha release
UCLID5 v0.9.1 Release
What's new?
- Support for mixing procedural and parallel modeling using primed variables.
- Simplified syntax by removing '::' and '->' operators and replacing them with '.'
- Support for constant literals and their use in for loops.
- Verifier bugfixes.
uclid5 v0.9.0 alpha release
New to this release:
- Support for (bounded) model checking of LTL properties.
- Added the define keyword for defining macros.
- Performance improvements in the VC generator.
- Lots and lots of bugfixes.