ftsrg
Support Boogie as a new CFA frontend
[Feature Request]
The aim of this feature request is to provide an alternative syntax or frontend to the currently used CFA grammar. Although the CFA grammar is fairly close to Theta's inner representation, thereby making debugging easier, it is difficult to read and even more difficult to write by hand.
On the other hand, Boogie is a well-known and widely used intermediate language for verification tools. Multiple frontends exist that emit Boogie code (for example), so consuming Boogie code would widen the circle of supported languages. Moreover, Boogie syntax is much more easier to read and write than the current CFA grammar, so supporting it would make the cfa-cli tool much more user friendly.
Agreed. First, we should start with the case where there is only a single Boogie procedure. As we discussed in person with @as3810t, this can be mapped to a single CFA in a mostly straightforward way. This would already be useful for writing test cases or to demonstrate Theta in education.
In the next step, we could move on to multiple Boogie procedures. Theta CFA does not support procedure calls, but we could apply modular verification: there would be a separate CFA for each procedure, where calls are replaced by specs (assert pre, havoc vars, assume post). Here, a design decision is whether to implement this directly in the cfa-cli tool (run an individual CEGAR for all CFAs) or as an external tool that calls cfa-cli multiple times (with each CFA).
