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

[Jesper Bengtson]

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.

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.

/Jesper

On 11 Oct 2018, at 05:28, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr<mailto:jeehoon.kang at sf.snu.ac.kr>> 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.

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

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.mpi-sws.org/pipermail/iris-club/attachments/20181011/09813cd0/attachment-0001.html>