<div dir="ltr"><div dir="auto">Thanks everyone from the comments. <div dir="auto"><br></div><div dir="auto">Generally, it sounds like there is a great deal of interest in it, but (currently) not a lot of work except for Robbert's work on C.</div><div dir="auto"><br></div><div dir="auto">As far as automation, it should be possible to re-use a lot of automation across these languages if we translate to VCs in heap_lang (or another core language). From Bedrock 1, I would imagine a CPS language (perhaps similar to what RustBelt did). I imagine that Iris in it's full generality would be difficulty to automate, but the ability to automate the "boring, non-concurrent" fragment of imperative programs would have a tremendous bang-for-the-buck and falling back on MosSel/IPM (which seem pretty good from my, admittedly limited, uses) for the complex reasoning would be pretty reasonable in my mind.</div><div dir="auto"><br></div><div>@Jesper I agree that the VST folks have done a lot here which is great and they have developed good automation. My interest in Iris is, to a large extent, related to its portability. It seems concievable (though not currently done) that one could do what you suggest and instantiate Iris on top of Jensen's work and integrate assembly code with C code in a single logical framework. VST, on the other hand, seems a bit more specialized to the C operational model. Perhaps you can still do this, and I'd be interested in work along these lines, but it seems like a bit more of a leap. As Jeehoon mentioned, weak memory is another feature that Iris supports (in theory?).<br></div><div dir="auto"><br></div><div dir="auto">@Robbert, I'd be interested in chatting with you a bit about your work. 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?</div></div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Oct 11, 2018, 4:40 AM Robbert Krebbers <<a href="mailto:mail@robbertkrebbers.nl" target="_blank">mail@robbertkrebbers.nl</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi Gregory,<br>
<br>
Together with Dan Frumin and Leon Gondelmann at Radboud University <br>
Nijmegen, I'm working on instantiating Iris with a C language. <br>
Currently, we are working on automation for non-determinism in <br>
expressions. In short: we have developed a new version of the logic from <br>
my POPL'14 paper in Iris that's better suited for automation. On top of <br>
that new logic, we are building automated tactics (by computational <br>
reflection) for computing verification conditions automatically.<br>
<br>
We eventually would like to support more features of C. First and <br>
foremost, if we want it to be actually usable, we need support for data <br>
types (all the different integer types, structs, unions, arrays). Right <br>
now, we use mathematical integers, and only have limited support for <br>
arrays (no structs and unions). For this, we could probably learn a lot <br>
from VST. Apart from that, we would like to support concurrency eventually.<br>
<br>
Best,<br>
<br>
Robbert<br>
<br>
On 10/10/18 10:39 PM, Gregory Malecha wrote:<br>
> Hello --<br>
> <br>
> I'm wondering how much work there has been applying Iris to reason about <br>
> "real-world" languages. I was really impressed with the RustBelt work, <br>
> and was wondering if there has been any work applying it to build <br>
> program logics on top of languages such as C, C++, Rust, or even assembly.<br>
> <br>
> Any pointers would be greatly appreciated. Even if there isn't any work <br>
> right now, if there is anyone interested either in producing or <br>
> consuming this sort of work, it would be great to know about interest.<br>
> <br>
> Thank you.<br>
> <br>
> -- <br>
> gregory malecha<br>
> <a href="http://gmalecha.github.io" rel="noreferrer noreferrer" target="_blank">gmalecha.github.io</a> <<a href="https://gmalecha.github.io" rel="noreferrer noreferrer" target="_blank">https://gmalecha.github.io</a>><br>
> <br>
<br>
-- <br>
<a href="mailto:iris-club@lists.mpi-sws.org" rel="noreferrer" target="_blank">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br>
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer noreferrer" target="_blank">https://lists.mpi-sws.org/listinfo/iris-club</a><br>
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" rel="noreferrer" target="_blank">iris-club-unsubscribe@lists.mpi-sws.org</a><br>
</blockquote></div>