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...

Descripción completa

Detalles Bibliográficos

Publicado en:	Communications of the ACM Vol. 54; no. 12; pp. 123 - 132
Autores principales:	Yang, Jean, Hawblitzel, Chris
Formato:	Artículo
Publicado:	Association for Computing Machinery Dec2011
Materias:	Assembly languages (Electronic computers) Hoare logic Computer programming Computer operating systems C# (Computer program language) Debugging
Acceso en línea:	Ver este registro en EBSCOhost