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 |
Conference DaySat 25 JanDisplayed time zone: Saskatchewan, Central America change
Conference Day
Sat 25 JanDisplayed time zone: Saskatchewan, Central America change
10:30 - 12:30 | |||
10:30 30mTalk | Deriving Instances with Dependent Types CoqPL Arthur Azevedo de AmorimCarnegie Mellon University, USA File Attached | ||
11:00 30mTalk | The use of Coq for Common Criteria Evaluations CoqPL File Attached | ||
11:30 30mTalk | Verifying concurrent Go code in Coq with Goose CoqPL 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 30mTalk | A Tutorial on Equations CoqPL Matthieu SozeauInria Media Attached File Attached | ||