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

[Jeehoon Kang]

Dear Jesper,

> Is there a particular reason you want to use Iris for this rather than
VST on its own.

Because it seems Iris has a potential to support weak memory model---as
iGPS shows---while VST deals with a substantial subset of C.
I basically want to enjoy the benefits of those at the same time.  I didn't
know about Robbert's work, but it looks very promising!

Thanks,
Jeehoon


2018년 10월 11일 (목) 오후 8:58, Ralf Jung <jung at mpi-sws.org>님이 작성:

> 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>
> >
>


-- 
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>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181011/5a3936d2/attachment.html>