Imagen de Portada
Código QR

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

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