-
Notifications
You must be signed in to change notification settings - Fork 13
PGo SPLASH
adam-tg edited this page Nov 5, 2018
·
3 revisions
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/splash/abstract.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/