<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=utf-8">
</head>
<body style="word-wrap: break-word; -webkit-nbsp-mode: space; line-break: after-white-space;" class="">
Is there a particular reason you want to use Iris for this rather than VST on its own. They have put a lot of effort into making the automation for the separation logic work reasonably painlessly. Jensen, Benton, and Kennedy worked on x86 assembly in Coq with
a program logic for that. It was quite impressive but I don’t believe anyone is working on that at the moment. Again, if you want that to work within Iris then there is quite a bit of work required.
<div class=""><br class="">
</div>
<div class="">So, to my knowledge RustBelt is the only work that uses “real” programming languages and Iris at the moment. I’d need to know a bit more about what you all want to do with it.</div>
<div class=""><br class="">
</div>
<div class="">/Jesper<br class="">
<div><br class="">
<blockquote type="cite" class="">
<div class="">On 11 Oct 2018, at 05:28, Jeehoon Kang <<a href="mailto:jeehoon.kang@sf.snu.ac.kr" class="">jeehoon.kang@sf.snu.ac.kr</a>> wrote:</div>
<br class="Apple-interchange-newline">
<div class="">
<div dir="ltr" class="">
<div class="">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.</div>
<div class=""><br class="">
</div>
<div class="">Thanks,</div>
<div class="">Jeehoon<br class="">
</div>
</div>
<br class="">
<div class="gmail_quote">
<div dir="ltr" class="">2018년 10월 11일 (목) 오전 5:41, Gregory Malecha <<a href="mailto:gmalecha@gmail.com" class="">gmalecha@gmail.com</a>>님이 작성:<br class="">
</div>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
<div dir="ltr" class="">Hello --
<div class=""><br class="">
</div>
<div class="">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.</div>
<div class=""><br class="">
</div>
<div class="">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.</div>
<div class=""><br class="">
</div>
<div class="">Thank you.</div>
<div class="">
<div class=""><br class="">
</div>
-- <br class="">
<div dir="ltr" class="m_-5891336899124328609gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr" class="">
<div class="">
<div dir="ltr" class="">
<div class="">gregory malecha</div>
<div class=""><a href="https://gmalecha.github.io/" target="_blank" class="">gmalecha.github.io</a></div>
</div>
</div>
</div>
</div>
</div>
</div>
-- <br class="">
<a href="mailto:iris-club@lists.mpi-sws.org" target="_blank" class="">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br class="">
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" rel="noreferrer" target="_blank" class="">
https://lists.mpi-sws.org/listinfo/iris-club</a><br class="">
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" target="_blank" class="">
iris-club-unsubscribe@lists.mpi-sws.org</a><br class="">
</blockquote>
</div>
<br clear="all" class="">
<br class="">
-- <br class="">
<div dir="ltr" class="gmail_signature" data-smartmail="gmail_signature">
<div dir="ltr" class=""><a href="http://sf.snu.ac.kr/jeehoon.kang" target="_blank" class="">Jeehoon Kang (Ph.D. student)</a>
<div class=""><a href="http://sf.snu.ac.kr/" target="_blank" class="">Software Foundations Laboratory</a>
<div class=""><a href="http://www.snu.ac.kr/" target="_blank" class="">Seoul National University</a></div>
</div>
</div>
</div>
-- <br class="">
<a href="mailto:iris-club@lists.mpi-sws.org" class="">iris-club@lists.mpi-sws.org</a> - Mailing List for the Iris Logic<br class="">
Management: <a href="https://lists.mpi-sws.org/listinfo/iris-club" class="">https://lists.mpi-sws.org/listinfo/iris-club</a><br class="">
Unsubscribe: <a href="mailto:iris-club-unsubscribe@lists.mpi-sws.org" class="">iris-club-unsubscribe@lists.mpi-sws.org</a><br class="">
</div>
</blockquote>
</div>
<br class="">
</div>
</body>
</html>