Verifying Distributed Systems with Concurrent Separation Logic
Distributed systems are the foundation of cloud computing and bugs in them can lead to outages of major providers and their customers. Unfortunately distributed systems are also hard to get right because they must handle concurrency, crash recovery, replication, and reconfiguration, which interact in subtle ways. A promising approach to verifying such systems (and thereby systematically eliminating classes of bugs) is based on concurrent separation logic, which allows components to be verified independently yet handle tricky interaction between components.
About Byte Bites
Byte Bites are informal gatherings open to CSAIL Alliances members and students who would like to attend a discussion on a current project. Most lunches or afternoon teas will feature a Faculty Researcher but a few will feature a PhD student, post-doc or Research Scientist.
