Safe to the last instruction.

Typed assembly language (TAL) and Hoare logic can be used to verify the absence of many kinds of errors in low-level code. We use TAL and Hoare logic to achieve highly automated, static verification of the safety of a new operating system called Verve. We have developed techniques and tools to mecha...

Full description

Bibliographic Details

Published in:	Communications of the ACM Vol. 54; no. 12; pp. 123 - 132
Main Authors:	Yang, Jean, Hawblitzel, Chris
Format:	Article
Published:	Association for Computing Machinery Dec2011
Subjects:	Assembly languages (Electronic computers) Hoare logic Computer programming Computer operating systems C# (Computer program language) Debugging
Online Access:	View this record in EBSCOhost