llrêve – non-interference –

Automatically check non-interference for C programs

Developed and maintained as part of the IMPROVE project by Mattias Ulbrich, Vladimir Klebanov and Moritz Kiefer.



(examples suffixed with ! contain programs that do have illegal information flow)

or enter a program:

Parameters which are "low":
Program:

Your program is sent to the server. Please be a little patient for the answer …
Checking
Running llrêve
Running Eldarica
SMT2 Code:

Counterexample

Counterexample

llrêve automatically check non-interference for C programs. For details take a look at the Usage page.