[Iris-Club] Iris on top of "real-world" languages

[Robbert Krebbers]

Hi Gregory,

Together with Dan Frumin and Leon Gondelmann at Radboud University 
Nijmegen, I'm working on instantiating Iris with a C language. 
Currently, we are working on automation for non-determinism in 
expressions. In short: we have developed a new version of the logic from 
my POPL'14 paper in Iris that's better suited for automation. On top of 
that new logic, we are building automated tactics (by computational 
reflection) for computing verification conditions automatically.

We eventually would like to support more features of C. First and 
foremost, if we want it to be actually usable, we need support for data 
types (all the different integer types, structs, unions, arrays). Right 
now, we use mathematical integers, and only have limited support for 
arrays (no structs and unions). For this, we could probably learn a lot 
from VST. Apart from that, we would like to support concurrency eventually.

Best,

Robbert

On 10/10/18 10:39 PM, Gregory Malecha wrote:
> Hello --
> 
> I'm wondering how much work there has been applying Iris to reason about 
> "real-world" languages. I was really impressed with the RustBelt work, 
> and was wondering if there has been any work applying it to build 
> program logics on top of languages such as C, C++, Rust, or even assembly.
> 
> Any pointers would be greatly appreciated. Even if there isn't any work 
> right now, if there is anyone interested either in producing or 
> consuming this sort of work, it would be great to know about interest.
> 
> Thank you.
> 
> -- 
> gregory malecha
> gmalecha.github.io <https://gmalecha.github.io>
>