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

Robbert Krebbers mail at robbertkrebbers.nl
Thu Oct 11 10:39:36 CEST 2018

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.



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>

More information about the Iris-Club mailing list