[Iris-Club] Iris on top of "real-world" languages
mail at robbertkrebbers.nl
Fri Oct 12 13:04:36 CEST 2018
On 10/11/18 9:29 PM, Gregory Malecha wrote:
> @Robbert, I'd be interested in chatting with you a bit about your
That certainly would be possible, I'll mail you in private about that.
> VST operates on Clight rather than the full language to avoid the
> complexities of evaluation strategies. If you were to plug into
> CompCert, you could do something similar. I guess plugging into
> another compiler would be more problematic, but it is still the case
> that Clight programs are also C programs so you could run your
> favorite compiler on the Clight code (rather than the source C).
> Would making that simplification make the task easier?
The primary motivation of our work is indeed that the verification is
sound w.r.t. any compiler; not just CompCert.
As you said, one could translate each C program into a version in which
all sequencing has been made explicit, and then use that program for
both the verification and as the input of your favorite C compiler. I
don't find this satisfactory. In the end of the day, it would be much
nicer if one could verify C programs as if, without having to modify the
source code of the program.
Besides, a program logic as the one we develop for C in Iris cannot just
be used for proving properties of concrete programs, but it can also be
used (typically by building logical relations) for different purposes, e.g.:
- Proving correctness of program transformations
- Proving correctness of say static analyses
In both of these cases you cannot modify the source programs.
More information about the Iris-Club