Different Abstract Domains in SILVA
val-co opened this issue · 5 comments
Hello, in the AAAI paper, I read that SILVA can be instantiated with different abstract domains such as Polyhedra. Can you please show me an example (using code) of how I can use the polyhedra input domain with SILVA? Thanks!
Hi,
adding more domains is possible, although a bit convoluted. Currently only hyperrectangles (aka boxes) are natively implemented.
To support different abstractions, one must either implement them in silva or (most likely) add bindings to existing libraries, such as the Parma Polyheadra Library. The relevant modifications involve src/abstract_domains and src/abstract_interpreters, as well as some minor changes in auxiliary files (e.g. the command line option parser to be able to read which abstract domain to use).
However, silva is already complete when using infinity norm perturbations (i.e. rectangles) and hard univariate trees/forests, thus making the use of other abstract domains redundant (and ironically worse, due to the longer execution times of non-interval abstractions). To exploit benefits of other domains, one should also further modify silva to deal with non-rectangular perturbations or non hard univariate trees/forests.
Closed for inactivity.
Sorry for the delay in getting back to you. The reason for the alternative domain is the desired expressiveness during the verification process. Some of my specifications look like a+b<=1, which I cannot define using the interval domain. In your response, you mention: "To exploit benefits of other domains, one should also further modify silva to deal with non-rectangular perturbations or non hard univariate trees/forests"
To that end, what additional specific files must be edited in SILVA in addition to src/abstract_domains and src/abstract_interpreters?
I see, other than src/abstract_domains and src/abstract_interpreters changes are needed in src/perturbation.h and src/perturbation.c to define the new type of perturbation, and src/options.c to parse the new perturbation type as a command line argument. src/abstract_domains/abstract_domain.h to declare the new type of abstract domain, src/abstract_classifier.c to decide which implementation of the classifier to use (in this case, the new polyhedral classifier, which will be implemented in src/abstract_interpreters/).
If I understand correctly the type of constraints within the tree is not subject to changes (i.e. they will stay in the form x_i < k) so it should not be necessary to modify other files.
Yes, the trees being used are still univariate, so the constraints in the trees won't change. The domain used along with new perturbation expressions are needed!