Abstract
dc:description.abstractGoose is a tool for translating a subset of the Go programming language into Perennial/Iris, which is an extension of Coq. However, Goose did not support channels, which are an important synchronization tool that Go is well known for. This thesis presents an extension to Goose to support channels, including a model to represent Go channels and operations in GooseLang, the language defined in Perennial/Iris that Goose translates into, an extension to the Goose translator to support channels, and a library of separation logic specifications that define the expected behavior of channel operations on open channels. Finally, this thesis evaluates how effective this model and library is for verifying Go code containing channels, and discuss some limitations and potential future work.
Degree
thesis:*- Name thesis:degree_name
- Master
- Department dc:contributor.department
- Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science
- Grantor dc:publisher
- Massachusetts Institute of Technology
- Year dc:date.issued
- 2025
Author and committee
dc:creator, dc:contributor.*- Author dc:creator
-
- Zhang, Jessica
- Advisor dc:contributor.advisor
-
- Zeldovich, Nickolai
Rights
dc:rights- Statement dc:rights
-
- In Copyright - Educational Use Permitted
- Copyright retained by author(s)
- Licence dc:rights.uri
Identifiers
dc:identifier.*- Handle dc:identifier.uri
- https://hdl.handle.net/1721.1/159079
- OAI identifier oai:identifier
- oai:dspace.mit.edu:1721.1/159079