Abstract
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.
Author supplied keywords
Cite
CITATION STYLE
Ioannidis, E., Kaashoek, F., & Zeldovich, N. (2019). Extracting and optimizing formally verified code for systems programming. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 11460 LNCS, pp. 228–236). Springer Verlag. https://doi.org/10.1007/978-3-030-20652-9_15
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
