No way to access AGREE as external analysis from Resolute

[kfhoech]

Issue by kfhoech
Tuesday Mar 06, 2018 at 15:13 GMT
Originally opened as smaccm/smaccm#90

---

Resolute presently has registered extensions for a simple thread schedule and a ngrep search.

Add and register a new extension implementing a call to AGREE.

There are a few complications:

1. Resolute already has an instance model to traverse. AGREE in a protected method wants to recreate its own instance. Need to resolve how interfaces need to be changed such that the instance from Resolute might be used by AGREE.
2. Analysis in AGREE may depend on property values set at higher layers of the analysis hierarchy. But the call from Resolute may reference an instance at a lower layer where the property values are not set. Or, perhaps this is handled appropriately merely by passing instance models rather than static implementation models. Need to investigate.
3. How should the results from AGREE be presented and collected into an aggregate result. Resolute may wish to access only one or a few guarantees or lemmas. How is this done? Since AGREE analysis may be computationally intensive, how can we share results from a single AGREE job with multiple Resolute external analysis calls?