Re: Formal description of system call interface

On Mon, Nov 21, 2016 at 7:14 AM, Dmitry Vyukov [off-list ref] wrote:

Re more complex side effects. I always feared that a description suitable
for automatic verification (i.e. zero false positives, otherwise it is useless)
may be too difficult to achieve.

Cyril, Tavis, can you come up with some set of predicates that can be
checked automatically yet still useful?
We can start small, e.g. "must not alter virtual address space".

Yes, I've been working on creating something like this, I have a
simple working prototype. I cant promise it has zero false positives
right now, but I think that is achievable.

Let me dig it up (I had put it on the back burner).

Tavis.