> On 26 Jun 2015, at 21:30, Anil Madhavapeddy <[email protected]> wrote: > > This one came out of the blue to me, but I noticed it in a tweet from Ranjit > Jhala. MPI folk have combined refinement types and (concurrent) separation > logic in order to verify properties about Lwt. > > Their test case? Dave Scott's OCaml FAT implementation that we use in > MirageOS. Spoiler: they found bugs :-)
Impossible, that code is 100% bug-free ;-) > http://drops.dagstuhl.de/opus/volltexte/2015/5223/pdf/13.pdf > > I'm still reading through it but thought I'd get it out to the list early… A little light reading for the weekend… Cheers, Dave > -anil > > > _______________________________________________ > MirageOS-devel mailing list > [email protected] > http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel _______________________________________________ MirageOS-devel mailing list [email protected] http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel
