595E - The Provable Properties of Mixed Hardware/Software Systems

The Provable Properties of Mixed Hardware/Software Systems:  A reading
group examining the ongoing research question of how formal analysis
techniques can be applied across the hardware/software system stack
from the microarchitecture and gate-level implementation, through the
ISA, OS, Compiler, and up to the layer of applications.  Examples
include provably correct cache coherence schemes, provable security
properties in custom microprocessors, and hardware design languages
with well defined operational semantics.