Releases · hopv/hoice

The main new feature in this release is support for datatypes. While functional, reasoning on datatypes is still a bit coarse and needs more work. For more information see the datatype wiki page.

Besides the various improvements and bug fixes, this release also packs a notion of unsat proof. More precisely, in case of unsat hoice can produce entry points. These are arguments for predicates appearing in positive clauses (clauses that have no predicate application in their body) that lead to a conflict. It was implemented with deterministic program verification in mind, meaning that if the clauses encode non-deterministic behavior then the entry point reconstruction i) might fail or ii) might allow more traces than the one leading to the conflict that hoice discovered. For more information see the unsat proofs wiki page.

Assets 3