seahorn/crab

Add a logico-numerical abstract domain

caballa opened this issue · 3 comments

From @caballa on October 15, 2016 23:32

One simple option is to integrate BDDApron but it is implemented in OCaml so it will add more dependencies to Crab and it would still require changes for supporting Crab domains.

Instead, I prefer to re-implement BDDApron by combining the ADD library (MTBDD) provided by CUDD with the existing Crab domains.

Copied from original issue: caballa/crab#6

We have implemented a reduced product of a numerical domain with a simple flat 3-valued boolean domain (see beb705f). This is less precise that the above described MTBDD-based domain but it is very cheap.

The boxes domain can also reason about Booleans.

We also have boxes so I close for now this issue.