{"id":{"repo_id":"mit","oai_identifier":"oai:dspace.mit.edu:1721.1/159079"},"canonical_url":"https://search.dev.ndltd.org/etd/mit/oai:dspace.mit.edu:1721.1/159079","repository":{"repo_id":"mit","name":"MIT","base_url":"https://dspace.mit.edu/oai/request"},"display":{"title":"Verification of Go Channels","abstract":"Goose 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.","abstract_html":"Goose 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.","abstract_has_math":false,"creators":["Zhang, Jessica"],"institution":"Massachusetts Institute of Technology","degree_name":"Master","degree_level":null,"degree_discipline":null,"degree_department":"Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science","school":null,"contributors":[],"advisors":["Zeldovich, Nickolai"],"committee_chairs":[],"committee_members":[],"year":2025,"date_issued":"2025-02","date_published":"2025-02","updated_at":"2026-07-22T22:21:54Z","subjects":[],"languages":[],"rights":["In Copyright - Educational Use Permitted","Copyright retained by author(s)"],"rights_urls":["https://rightsstatements.org/page/InC-EDU/1.0/"],"identifier_entries":[]},"links":{"outbound_url":"https://hdl.handle.net/1721.1/159079","outbound_label":"Handle","outbound_source":"dc:identifier.uri"},"metadata_groups":[{"id":"people","label":"People","entries":[{"key":"dc:contributor.advisor","label":"Advisor","values":["Zeldovich, Nickolai"]},{"key":"dc:contributor.department","label":"Department","values":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"]},{"key":"dc:creator","label":"Author","values":["Zhang, Jessica"]}]},{"id":"academic_context","label":"Academic Context","entries":[{"key":"dc:date.accessioned","label":"Dc Date Accessioned","values":["2025-04-14T14:04:14Z"]},{"key":"dc:date.available","label":"Dc Date Available","values":["2025-04-14T14:04:14Z"]},{"key":"dc:date.issued","label":"Date","values":["2025-02"]},{"key":"dc:publisher","label":"Institution","values":["Massachusetts Institute of Technology"]},{"key":"dc:type","label":"Dc Type","values":["Thesis"]},{"key":"thesis:degree_name","label":"Degree Name","values":["Master","Master of Engineering in Electrical Engineering and Computer Science"]}]},{"id":"language_rights","label":"Language and Rights","entries":[{"key":"dc:rights","label":"Dc Rights","values":["In Copyright - Educational Use Permitted","Copyright retained by author(s)"]},{"key":"dc:rights.uri","label":"Rights URI","values":["https://rightsstatements.org/page/InC-EDU/1.0/"]}]},{"id":"identifiers","label":"Identifiers","entries":[{"key":"dc:identifier.uri","label":"Identifier URI","values":["https://hdl.handle.net/1721.1/159079"]}]},{"id":"additional","label":"Additional Metadata","entries":[{"key":"dc:description.abstract","label":"Abstract","values":["Goose 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."]},{"key":"dc:description.degree","label":"Dc Description Degree","values":["M.Eng."]},{"key":"dc:title","label":"Title","values":["Verification of Go Channels"]}]}],"canonical_facts":{"dc:contributor.advisor":["Zeldovich, Nickolai"],"dc:contributor.department":["Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science"],"dc:creator":["Zhang, Jessica"],"dc:date.accessioned":["2025-04-14T14:04:14Z"],"dc:date.available":["2025-04-14T14:04:14Z"],"dc:date.issued":["2025-02"],"dc:description.abstract":["Goose 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."],"dc:description.degree":["M.Eng."],"dc:identifier.uri":["https://hdl.handle.net/1721.1/159079"],"dc:publisher":["Massachusetts Institute of Technology"],"dc:rights":["In Copyright - Educational Use Permitted","Copyright retained by author(s)"],"dc:rights.uri":["https://rightsstatements.org/page/InC-EDU/1.0/"],"dc:title":["Verification of Go Channels"],"dc:type":["Thesis"],"thesis:degree_name":["Master","Master of Engineering in Electrical Engineering and Computer Science"]},"updated_at":"2026-07-22T22:21:54Z"}