Extracting and Optimizing Formally Verified Code for Systems Programming
MCQC is a compiler for extracting verified systems programs to low-level assembly, with no runtime or garbage collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17,...
| Main Authors: | , , |
|---|---|
| Other Authors: | |
| Format: | Book |
| Language: | English |
| Published: |
Springer International Publishing
2020
|
| Online Access: | https://hdl.handle.net/1721.1/125251 |
| _version_ | 1811069818979221504 |
|---|---|
| author | Ioannidis, Eleftherios Kaashoek, M. Frans Zeldovich, Nickolai |
| author2 | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| author_facet | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science Ioannidis, Eleftherios Kaashoek, M. Frans Zeldovich, Nickolai |
| author_sort | Ioannidis, Eleftherios |
| collection | MIT |
| description | MCQC is a compiler for extracting verified systems programs to low-level assembly, with no runtime or garbage collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a few memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions separately MCQC can generate executable verified code directly from Gallina, reducing the effort of implementing and executing verified systems. Keywords: Formal verification; Functional compiler; Extraction; Systems |
| first_indexed | 2024-09-23T08:16:44Z |
| format | Book |
| id | mit-1721.1/125251 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T08:16:44Z |
| publishDate | 2020 |
| publisher | Springer International Publishing |
| record_format | dspace |
| spelling | mit-1721.1/1252512022-09-23T12:05:30Z Extracting and Optimizing Formally Verified Code for Systems Programming Ioannidis, Eleftherios Kaashoek, M. Frans Zeldovich, Nickolai Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science MCQC is a compiler for extracting verified systems programs to low-level assembly, with no runtime or garbage collection requirements and an emphasis on performance. MCQC targets the Gallina functional language used in the Coq proof assistant. MCQC translates pure and recursive functions into C++17, while compiling monadic effectful functions to imperative C++ system calls. With a few memory and performance optimizations, MCQC combines verifiability with memory and runtime performance. By handling effectful and pure functions separately MCQC can generate executable verified code directly from Gallina, reducing the effort of implementing and executing verified systems. Keywords: Formal verification; Functional compiler; Extraction; Systems 2020-05-14T19:59:57Z 2020-05-14T19:59:57Z 2019-05 2019-07-08T17:28:09Z Book http://purl.org/eprint/type/ConferencePaper 9783030206512 9783030206529 0302-9743 1611-3349 https://hdl.handle.net/1721.1/125251 Ioannidis, Eleftherios, Frans Kaashoek, and Nickolai Zeldovich. "Extracting and Optimizing Formally Verified Code for Systems Programming." NASA Formal Methods, NFM 2019, edited by Badger J., Rozier K., Springer, Cham, 2019 en http://dx.doi.org/10.1007/978-3-030-20652-9_15 NASA Formal Methods Symposium 2019 Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Springer International Publishing MIT web domain |
| spellingShingle | Ioannidis, Eleftherios Kaashoek, M. Frans Zeldovich, Nickolai Extracting and Optimizing Formally Verified Code for Systems Programming |
| title | Extracting and Optimizing Formally Verified Code for Systems Programming |
| title_full | Extracting and Optimizing Formally Verified Code for Systems Programming |
| title_fullStr | Extracting and Optimizing Formally Verified Code for Systems Programming |
| title_full_unstemmed | Extracting and Optimizing Formally Verified Code for Systems Programming |
| title_short | Extracting and Optimizing Formally Verified Code for Systems Programming |
| title_sort | extracting and optimizing formally verified code for systems programming |
| url | https://hdl.handle.net/1721.1/125251 |
| work_keys_str_mv | AT ioannidiseleftherios extractingandoptimizingformallyverifiedcodeforsystemsprogramming AT kaashoekmfrans extractingandoptimizingformallyverifiedcodeforsystemsprogramming AT zeldovichnickolai extractingandoptimizingformallyverifiedcodeforsystemsprogramming |