Skip to content

v2.4.0
Compare
Choose a tag to compare
@hajduakos hajduakos released this 10 Sep 07:36
· 3123 commits to master since this release
v2.4.0
949b632
This commit was created on GitHub.com and signed with GitHub’s verified signature. The key has expired.
GPG key ID: 4AEE18F83AFDEB23
Expired
Verified
Learn about vigilant mode.

This release adds algorithmic support to bitvectors in the theta-cfa-cli tool via new refinement strategies. Previous strategies (e.g., SEQ_ITP) did not work for bitvectors because the underlying Z3 solver does not support interpolation over bitvectors. The new strategies are based on unsat core predicates and the Newton approach. Note that these algorithms are still in an experimental phase, we are working on their benchmarking and fine-tuning. Credits go to @as3810t.

Assets 6
Loading