Releases: usi-verification-and-security/golem
v0.3.0
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
v0.1.1
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
Initial release