<div dir="ltr"><div>Dear Jesper,</div><div><br></div><div>> Is there a particular reason you want to use Iris for this rather than VST on its own.</div><div><br></div><div>Because it seems Iris has a potential to support weak memory model---as iGPS shows---while VST deals with a substantial subset of C.</div><div>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!</div><div><br></div><div>Thanks,</div><div>Jeehoon<br></div><div><br></div></div><br><div class="gmail_quote"><div dir="ltr">2018년 10월 11일 (목) 오후 8:58, Ralf Jung <<a href="mailto:jung@mpi-sws.org">jung@mpi-sws.org</a>>님이 작성:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
On 11.10.18 05:28, Jeehoon Kang wrote:<br>
> I'm also wondering if anyone is interested in Iris + VST :)  I'm eager to use<br>
> it, if exists, in verifying real-world concurrent programs.<br>
<br>
Very interested!  Using Iris to prove things about programs compiled with<br>
CompCert would be amazing.  The VST developers also expressed some interested in<br>
getting these worlds better connected.  It's a lot of work though...<br>
<br>
Kind regards,<br>
Ralf<br>
<br>
> <br>
> Thanks,<br>
> Jeehoon<br>
> <br>
> 2018년 10월 11일 (목) 오전 5:41, Gregory Malecha <<a href="mailto:gmalecha@gmail.com" target="_blank">gmalecha@gmail.com</a><br>
> <mailto:<a href="mailto:gmalecha@gmail.com" target="_blank">gmalecha@gmail.com</a>>>님이 작성:<br>
> <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, and<br>
>     was wondering if there has been any work applying it to build program logics<br>
>     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 consuming<br>
>     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" target="_blank">gmalecha.github.io</a> <<a href="https://gmalecha.github.io" rel="noreferrer" target="_blank">https://gmalecha.github.io</a>><br>
>     -- <br>
>     <a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a> <mailto:<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank">iris-club@lists.mpi-sws.org</a>> - Mailing<br>
>     List for the Iris Logic<br>
>     Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank">https://lists.mpi-sws.org/listinfo/iris-club</a><br>
>     Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mpi-sws.org</a><br>
>     <mailto:<a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank">iris-club-unsubscribe@lists.mpi-sws.org</a>><br>
> <br>
> <br>
> <br>
> -- <br>
> Jeehoon Kang (Ph.D. student) <<a href="http://sf.snu.ac.kr/jeehoon.kang" rel="noreferrer" target="_blank">http://sf.snu.ac.kr/jeehoon.kang</a>><br>
> Software Foundations Laboratory <<a href="http://sf.snu.ac.kr" rel="noreferrer" target="_blank">http://sf.snu.ac.kr</a>><br>
> Seoul National University <<a href="http://www.snu.ac.kr" rel="noreferrer" target="_blank">http://www.snu.ac.kr</a>><br>
> <br>
</blockquote></div><br clear="all"><br>-- <br><div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature"><div dir="ltr"><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank">Jeehoon Kang (Ph.D. student)</a><div><a href="http://sf.snu.ac.kr" target="_blank">Software Foundations Laboratory</a><div><a href="http://www.snu.ac.kr" target="_blank">Seoul National University</a></div></div></div></div>