PGo SPLASH

Abstract:

Distributed systems are difficult to design and implement correctly. There is a growing interest in specification (spec) languages for distributed systems, which can be checked exhaustively or proved to satisfy certain properties. For ex- ample, Amazon uses TLA+ and PlusCal in building its web services [9]. However, there is no way to generate an im- plementation of spec in one of these modeling languages. Towards this end, we are building PGo. The goal of PGo is to reduce developer burden by providing a mechanical transla- tion between an abstract spec and a concrete implementation.

Extended abstract:

https://github.com/UBC-NSS/pgo/blob/SPLASH/papers/SPLASHAbstract.pdf

Implementation:

https://github.com/UBC-NSS/pgo/

People:

• Matthew Do: https://www.linkedin.com/in/minhndo/
• Renato Costa: https://github.com/rmascarenhas
• Finn Hackett: TBD
• Brandon Zhang: TBD
• Yi Fan (Bob) Yang: TBD
• Adam Geller: https://www.cs.ubc.ca/~atgeller/
• Ivan Beschastnikh: https://www.cs.ubc.ca/~bestchai/