What is it about?
Distributed systems are hard to build correctly. As a result, systems in production often contain bugs. Developers often use formal verification tools but verification mostly happens in the design part, and the final implementation leaves unverified. Thus, there remains a gap between models of system design and runnable code. PGo bridges this gap by compiling verified distributed system models into implementations in the Go programming languages.
Featured Image
Photo by Taylor Vick on Unsplash
Why is it important?
PGo is a step towards having practical verified implementations of distributed systems. PGo requires less time to develop a verified system. Our evaluation shows that PGo-based systems have at least 40% better performance than verified systems state-of-the-art.
Read the Original
This page is a summary of: Compiling Distributed System Models with PGo, January 2023, ACM (Association for Computing Machinery),
DOI: 10.1145/3575693.3575695.
You can read the full text:
Resources
Contributors
The following have contributed to this page
