POPL 2020 (series) / CoqPL 2020 (series) / The Sixth International Workshop on Coq for Programming Languages /
Verifying concurrent Go code in Coq with Goose
This paper describes Goose, a subset of Go that can be translated to a Coq model. The Coq model plugs into Iris for concurrency proofs, giving an end-to-end system for writing and verifying concurrent systems. We have used Goose as part of our work on Perennial to verify a concurrent, crash-safe mail server that gets good performance.
| (coqpl20-final4.pdf) | 432KiB |
| Goose CoqPL 2020 - slides (goose coqpl2020-slides.pdf) | 321KiB |
Sat 25 Jan
| 10:30 - 11:00 Talk | Arthur Azevedo de AmorimCarnegie Mellon University, USA File Attached | |||||||||||||||||||||||||||||||||||||||||
| 11:00 - 11:30 Talk | File Attached | |||||||||||||||||||||||||||||||||||||||||
| 11:30 - 12:00 Talk | Tej ChajedMassachusetts Institute of Technology, USA, Joseph TassarottiBoston College, M. Frans KaashoekMassachusetts Institute of Technology, USA, Nickolai ZeldovichMassachusetts Institute of Technology, USA Link to publication File Attached | |||||||||||||||||||||||||||||||||||||||||
| 12:00 - 12:30 Talk | Matthieu SozeauInria Media Attached File Attached | |||||||||||||||||||||||||||||||||||||||||