Skip to content

UCLID5 v0.9.5b New Public Release

Pre-release
Pre-release
Compare
Choose a tag to compare
@pramodsu pramodsu released this 12 Jun 11:30
· 1830 commits to master since this release
v0.9.5b
c767615

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.

Assets 3
Loading