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: | Ioannidis, Eleftherios, Kaashoek, M. Frans, Zeldovich, Nickolai |
---|---|
Other Authors: | Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science |
Format: | Book |
Language: | English |
Published: |
Springer International Publishing
2020
|
Online Access: | https://hdl.handle.net/1721.1/125251 |
Similar Items
-
Extracting and optimizing low-level bytecode from high-level verified Coq
by: Ioannidis, Eleftherios Ioannis.
Published: (2019) -
Verifying concurrent, crash-safe systems with Perennial
by: Chajed, Tej, et al.
Published: (2021) -
Argosy: verifying layered storage systems with recovery refinement
by: Chajed, Tej, et al.
Published: (2021) -
Grove: a Separation-Logic Library for Verifying Distributed Systems
by: Sharma, Upamanyu, et al.
Published: (2023) -
VerSum: Verifiable Computations over Large Public Logs
by: van den Hooff, Jelle, et al.
Published: (2015)