Verifying concurrent Go code in Coq with Goose (CoqPL 2020 - The Sixth International Workshop on Coq for Programming Languages)

Write a Blog >>

Sun 19 - Sat 25 January 2020 New Orleans, Louisiana, United States

Who

Tej Chajed, Joseph Tassarotti, M. Frans Kaashoek, Nickolai Zeldovich

Track

CoqPL 2020

Time Zone

The program is currently displayed in (GMT-06:00) Saskatchewan, Central America.

Use conference time zone: (GMT-06:00) Saskatchewan, Central AmericaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

By setting a time band, the program will dim events that are outside this time window. This is useful for (virtual) conferences with a continuous program (with repeated sessions).
The time band will also limit the events that are included in the personal iCalendar subscription service.

Display full programSpecify a time band

Save

When

Sat 25 Jan 2020 11:30 - 12:00 at Maurepas - Contributed Talks Chair(s): Amin Timany

Abstract

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.

Link to Publication

https://www.chajed.io/papers/goose:coqpl2020.pdf

File attachments

(coqpl20-final4.pdf)	432KiB
Goose CoqPL 2020 - slides (goose coqpl2020-slides.pdf)	321KiB

Tej Chajed

Massachusetts Institute of Technology, USA

United States

Joseph Tassarotti

Boston College

M. Frans Kaashoek

Massachusetts Institute of Technology, USA

Nickolai Zeldovich

Massachusetts Institute of Technology, USA

Time Zone

The program is currently displayed in (GMT-06:00) Saskatchewan, Central America.

Use conference time zone: (GMT-06:00) Saskatchewan, Central AmericaSelect other time zone

The GMT offsets shown reflect the offsets at the moment of the conference.

Time Band

Display full programSpecify a time band

Save

Session Program

Sat 25 Jan
Times are displayed in time zone: Saskatchewan, Central America change

10:30 - 12:30	Contributed TalksCoqPL at Maurepas Chair(s): Amin Timanyimec-Distrinet KU-Leuven

10:30 30m Talk		Deriving Instances with Dependent Types CoqPL Arthur Azevedo de AmorimCarnegie Mellon University, USA File Attached
11:00 30m Talk		The use of Coq for Common Criteria Evaluations CoqPL Yves BertotINRIA, Maxime DénèsInria, Vincent LaporteInria, Arnaud FontaineANSSI, Thomas LetanANSSI File Attached
11:30 30m Talk		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 30m Talk		A Tutorial on Equations CoqPL Matthieu SozeauInria Media Attached File Attached