Extracting and Optimizing Formally Verified Code for Systems Programming
In: NASA Formal Methods Symposium 2019; 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; (2019)
Online
Buch
Zugriff:
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
| Titel: |
Extracting and Optimizing Formally Verified Code for Systems Programming
|
|---|---|
| Autor/in / Beteiligte Person: | Ioannidis, Eleftherios ; Kaashoek, M. Frans ; Zeldovich, Nickolai ; Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
| Link: | |
| Quelle: | NASA Formal Methods Symposium 2019; 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; (2019) |
| Veröffentlichung: | Springer International Publishing, 2019 |
| Medientyp: | Buch |
| ISBN: | 978-3-030-20651-2 (print) ; 978-3-030-20652-9 (print) ; 3-030-20651-3 (print) ; 3-030-20652-1 (print) |
| ISSN: | 0302-9743 (print) ; 1611-3349 (print) |
| DOI: | 10.1007/978-3-030-20652-9_15 |
| Sonstiges: |
|