ARMor: fully verified software fault isolation. - Lu Zhao 002; Guodong Li; Bjorn De Sutter; John Regehr (EMSOFT, 2011)

A Program Logic and Its Application in Fully Verified Software Fault Isolation. - Lu Zhao 002 (2012)