A Deep Specification for Dropbox - Benjamin Pierce

Benjamin Pierce presents a formal specification and random testing framework for verifying the core behavior of Dropbox.

Formal specification of software systems is an old endeavor that is now yielding striking successes, in large part due to the availability of powerful new techniques for coupling specifications with running code via formal verification or automated testing. This talk surveys what’s happening in the area broadly and presents one example in more detail: a formal specification of the core behavior of a synchronization service and a specification-based random testing framework for applying it to real-world synchronizers. About the speaker: Benjamin Pierce is Henry Salvatori Professor of Computer and Information Science at the University of Pennsylvania and a Fellow of the ACM. His research interests include programming languages, type systems, language-based security, computer-assisted formal verification, differential privacy, and synchronization technologies. He is the author of the widely used graduate textbooks Types and Programming Languages and Software Foundations. He has served as co-Editor in Chief of the Journal of Functional Programming, as Managing Editor for Logical Methods in Computer Science, and as editorial board member of Mathematical Structures in Computer Science, Formal Aspects of Computing, and ACM Transactions on Programming Languages and Systems. He is also the lead designer of the popular Unison file synchronizer.