Matvey Arye will present his master's thesis talk on Friday April 22 at 10AM in Room 301. His advisor is Mike Freedman. Everyone is welcome to attend his talk. His abstract follows below. ------------------------------- Abstract: Currently, the Internet does not support device mobility natively. If a device moves across layer-2 domains, there is no way to preserve connectivity for ongoing connections. Similarly, there is no support for using multiple points of attachment (e.g. WiFi and 3G) concurrently on a single connection. This talk introduces FlexMove, an in-band, formally verified, protocol that supports device mobility and introduces a flow abstraction that enables connections to use multiple points of attachment. This talk will also describe the problems encountered and lessons learned while modeling and verifying this protocol using a tool called SPIN.