A Verified Information-Flow Architecture

Commented Coq development (Basic Machine)

December, 2013

The complete sources can be downloaded from here (licence).


Contents

Entry point

Common definitions

Abstract machine

Symbolic abstract machine

Concrete machine

DSL compiler - Fault-handler generation