Plural, Fusion and Plaid: Protocols in Practice

Jonathan Aldrich, Carnegie Mellon University, USA

Over the last 6 years we have mined, specified and verified protocols in millions of lines of code in the Plural and Fusion projects, using both type system and program analysis techniques. This talk will describe the frequency and characteristics of protocols found in the wild, as well as the specification and verification features we have found necessary to capture and check those protocols in real-world code. I will close by discussing the preliminary design of Plaid, a programming language built from the ground up to support protocol specification and static and dynamic checking.