Skip to content

Releases: usi-verification-and-security/golem

v0.3.0

15 Dec 10:18
Compare
Choose a tag to compare

This release adds new engine to the supporting backend: IMC, the original interpolation-based model-checking algorithm from McMillan.
It was contributed by @BritikovKI.

Additionally, with this release, the Spacer engine now also produces proofs of unsatisfiability.
The output format of the unsatisfiability proof has been changed and now follows more closely the output format as printed by Eldarica.

v0.2.0

23 Nov 09:40
Compare
Choose a tag to compare

This release updates the dependency OpenSMT to version 2.4.3.
It also contains a small improvement to Spacer engine.

v0.1.1

29 Oct 10:18
Compare
Choose a tag to compare

This release contains an updated to latest version of OpenSMT (2.4.2) and it adds two reasoning engines to Golem: BMC and k-induction.
Both engines currently work only on transition systems.
BMC is the basic bounded model checking algorithm that utilizes incremental solving in OpenSMT to speed up the counterexample search.
K-induction engine implements very basic k-induction algorithm.

Version 0.1.0

16 May 20:13
Compare
Choose a tag to compare

Initial release