Extracting and optimizing low-level bytecode from high-level verified Coq
This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections.
Main Author: | Ioannidis, Eleftherios Ioannis. |
---|---|
Other Authors: | Frans Kaashoek and Nickolai Zeldovich. |
Format: | Thesis |
Language: | eng |
Published: |
Massachusetts Institute of Technology
2019
|
Subjects: | |
Online Access: | https://hdl.handle.net/1721.1/121675 |
Similar Items
-
Verifying information flow control in Java bytecodes
by: Mathewson, Nicholas A. (Nicholas Albert), 1977-
Published: (2014) -
CoqIOA : a formalization of IO automata in the Coq proof assistant
by: Athalye, Anish (Anish R.)
Published: (2017) -
Correct-by-construction finite field arithmetic in Coq
by: Philipoom, Jade (Jade D.)
Published: (2018) -
Crafting certified elliptic curve cryptography implementations in Coq
by: Erbsen, Andres
Published: (2017) -
Performance optimization of the VDFS verified file system
by: Konradi, Alexander V.
Published: (2018)