Formal Modeling and Analysis of Distributed Systems

Explore formal modeling and analysis techniques for distributed systems in this conference talk from Strange Loop 2022. Learn how the P programming framework addresses the challenges of designing, implementing, and testing complex distributed systems. Discover how formal methods can be integrated into all phases of the development process, from system design to production monitoring. Gain insights into the application of P in industry and academia, including its use in Amazon Web Services' S3 Strong Consistency project. Understand the importance of abstract thinking and formal reasoning in tackling the complexities of distributed systems programming. Delve into topics such as the Two Phase Commit Protocol, model checking as a search problem, and strategies for uncovering deep bugs in distributed systems.

Intro
Programming Distributed Systems is Challenging!
Not uncommon to find bugs in production after deployment
Formal Methods to the Rescue!
Thinking abstractly, formally, above coding
Challenges with wide spread adoption of Formal Methods!
Formal Reasoning of S3 Strong Consistency Design using P
Two Phase Commit Protocol
P Tutorials and Documentation
Lessons Learned (P as a Thinking Tool)
Model Checking as a search problem
How to find deep bugs?