[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

  • To: mirageos-devel <mirageos-devel@xxxxxxxxxxxxxxxxxxxx>
  • From: Anil Madhavapeddy <anil@xxxxxxxxxx>
  • Date: Fri, 26 Jun 2015 21:30:20 +0100
  • Delivery-date: Fri, 26 Jun 2015 20:30:42 +0000
  • List-id: Developer list for MirageOS <mirageos-devel.lists.xenproject.org>

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


I'm still reading through it but thought I'd get it out to the list early...


MirageOS-devel mailing list



Lists.xenproject.org is hosted with RackSpace, monitoring our
servers 24x7x365 and backed by RackSpace's Fanatical Support®.