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

[Ralf Jung]

Hi,

On 11.10.18 05:28, Jeehoon Kang wrote:
> I'm also wondering if anyone is interested in Iris + VST :)  I'm eager to use
> it, if exists, in verifying real-world concurrent programs.

Very interested!  Using Iris to prove things about programs compiled with
CompCert would be amazing.  The VST developers also expressed some interested in
getting these worlds better connected.  It's a lot of work though...

Kind regards,
Ralf

> 
> Thanks,
> Jeehoon
> 
> 2018년 10월 11일 (목) 오전 5:41, Gregory Malecha <gmalecha at gmail.com
> <mailto:gmalecha at gmail.com>>님이 작성:
> 
>     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>
>     -- 
>     iris-club at lists.mpi-sws.org <mailto:iris-club at lists.mpi-sws.org> - Mailing
>     List for the Iris Logic
>     Management: https://lists.mpi-sws.org/listinfo/iris-club
>     Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>     <mailto:iris-club-unsubscribe at lists.mpi-sws.org>
> 
> 
> 
> -- 
> Jeehoon Kang (Ph.D. student) <http://sf.snu.ac.kr/jeehoon.kang>
> Software Foundations Laboratory <http://sf.snu.ac.kr>
> Seoul National University <http://www.snu.ac.kr>
>