Re: [MirageOS-devel] asynchronous liquid separation types paper: finding bugs in OCaml FAT

[Dave Scott <Dave.Scott@xxxxxxxxxx>]

> On 26 Jun 2015, at 21:30, Anil Madhavapeddy <anil@xxxxxxxxxx> 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
> MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
> http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel

_______________________________________________
MirageOS-devel mailing list
MirageOS-devel@xxxxxxxxxxxxxxxxxxxx
http://lists.xenproject.org/cgi-bin/mailman/listinfo/mirageos-devel