| dc.contributor |
Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
|
| dc.creator |
Ioannidis, Eleftherios |
|
| dc.creator |
Kaashoek, M. Frans |
|
| dc.creator |
Zeldovich, Nickolai |
|
| dc.date |
2020-05-14T19:59:57Z |
|
| dc.date |
2020-05-14T19:59:57Z |
|
| dc.date |
2019-05 |
|
| dc.date |
2019-07-08T17:28:09Z |
|
| dc.date.accessioned |
2023-03-01T18:10:55Z |
|
| dc.date.available |
2023-03-01T18:10:55Z |
|
| dc.identifier |
9783030206512 |
|
| dc.identifier |
9783030206529 |
|
| dc.identifier |
0302-9743 |
|
| dc.identifier |
1611-3349 |
|
| dc.identifier |
https://hdl.handle.net/1721.1/125251 |
|
| dc.identifier |
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 |
|
| dc.identifier.uri |
http://localhost:8080/xmlui/handle/CUHPOERS/279058 |
|
| dc.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 |
|
| dc.format |
application/pdf |
|
| dc.language |
en |
|
| dc.publisher |
Springer International Publishing |
|
| dc.relation |
http://dx.doi.org/10.1007/978-3-030-20652-9_15 |
|
| dc.relation |
NASA Formal Methods Symposium 2019 |
|
| dc.rights |
Creative Commons Attribution-Noncommercial-Share Alike |
|
| dc.rights |
http://creativecommons.org/licenses/by-nc-sa/4.0/ |
|
| dc.source |
MIT web domain |
|
| dc.title |
Extracting and Optimizing Formally Verified Code for Systems Programming |
|
| dc.type |
Book |
|
| dc.type |
http://purl.org/eprint/type/ConferencePaper |
|