Department of Computer Science and Technology

CHERI

Proofs for CHERI Concentrate


For the paper CHERI Concentrate: Practical Compressed Capabilities we constructed proofs for:

With the appropriate packages installed, these proofs can be run using Holmake:
 Holmake boundsTheory.uo
 Holmake compressTheory.uo