CoqIOA : a formalization of IO automata in the Coq proof assistant
Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2017
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/112831 |
| _version_ | 1826207046477807616 |
|---|---|
| author | Athalye, Anish (Anish R.) |
| author2 | M. Frans Kaashoek and Nickolai Zeldovich. |
| author_facet | M. Frans Kaashoek and Nickolai Zeldovich. Athalye, Anish (Anish R.) |
| author_sort | Athalye, Anish (Anish R.) |
| collection | MIT |
| description | Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017. |
| first_indexed | 2024-09-23T13:42:39Z |
| format | Thesis |
| id | mit-1721.1/112831 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:42:39Z |
| publishDate | 2017 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1128312019-04-10T08:00:28Z CoqIOA : a formalization of IO automata in the Coq proof assistant Athalye, Anish (Anish R.) M. Frans Kaashoek and Nickolai Zeldovich. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017. This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. Cataloged from student-submitted PDF version of thesis. Includes bibliographical references (pages 51-53). Implementing distributed systems correctly is difficult. Designing correct distributed systems protocols is challenging because designs must account for concurrent operation and handle network and machine failures. Implementing these protocols is challenging as well: it is difficult to avoid subtle bugs in implementations of complex protocols. Formal verification is a promising approach to ensuring distributed systems are free of bugs, but verification is challenging and time-consuming. Unfortunately, current approaches to mechanically verifying distributed systems in proof assistants using deductive verification do not allow for modular reasoning, which could greatly reduce the effort required to implement verified distributed systems by enabling reuse of code and proofs. This thesis presents CoqIOA, a framework for reasoning about distributed systems in a compositional way. CoqIOA builds on the theory of input/output automata to support specification, proof, and composition of systems within the proof assistant. The framework's implementation of the theory of IO automata, including refinement, simulation relations, and composition, are all machine-checked in the Coq proof assistant. An evaluation of CoqIOA demonstrates that the framework enables compositional reasoning about distributed systems within the proof assistant. by Anish Athalye. M. Eng. 2017-12-20T17:24:29Z 2017-12-20T17:24:29Z 2017 2017 Thesis http://hdl.handle.net/1721.1/112831 1015183848 eng MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission. http://dspace.mit.edu/handle/1721.1/7582 53 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Athalye, Anish (Anish R.) CoqIOA : a formalization of IO automata in the Coq proof assistant |
| title | CoqIOA : a formalization of IO automata in the Coq proof assistant |
| title_full | CoqIOA : a formalization of IO automata in the Coq proof assistant |
| title_fullStr | CoqIOA : a formalization of IO automata in the Coq proof assistant |
| title_full_unstemmed | CoqIOA : a formalization of IO automata in the Coq proof assistant |
| title_short | CoqIOA : a formalization of IO automata in the Coq proof assistant |
| title_sort | coqioa a formalization of io automata in the coq proof assistant |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/112831 |
| work_keys_str_mv | AT athalyeanishanishr coqioaaformalizationofioautomatainthecoqproofassistant |