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

[Anil Madhavapeddy <anil@xxxxxxxxxx>]

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 :-)

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

-anil


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