Relations for Incremental Verification

Sebastiaan Joosten

Incremental verification means that after making small changes to a program, annotations, and specifications, only a small part of the verification needs to be re-evaluated. As an extension of this: making a small change to a verification technique should also require only part of any verification to be re-evaluated. For this to work, we need a suitable domain specific language for verification techniques. A requirement for this language is that conceptually small changes should be likely to result in small code changes.

We propose to base such a language on binary (or bi-directional) relations, or equivalently: labeled directed graphs. The language has some well-known (semi)-decidable fragments, is very compositional, and can be typed in several ways. The talk combines some results from several earlier papers, but the proposed language is not a finished language. Instead, the talk is a call for feedback and collaboration: many details need to be worked out, including a first implementation of an interpreter.

---

Previous: Olaf Maas | Towards Language Parametric Web-Based Development Environments
Next: Gabriël Konat | Scalable Incremental Building with Dynamic Task Dependencies