Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
- Author
- YANG, Jean1 ; HAWBLITZEL, Chris2
[1] Massachusetts Institute of Technology, United States
[2] Microsoft Research, United States - Conference title
- Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)
- Conference name
- ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10) (PLDI'10) (Toronto, Ontario 2010-06-05)
- Author (monograph)
- Association for Computing Machinery (ACM), Special Interest Group on Programming Languages (SIGPLAN), New York, NY, United States (Organiser of meeting)
Association for Computing Machinery (ACM), Special Interest Group on Software Engineering (SIGSOFT), New York, NY, United States (Organiser of meeting) - Source
ACM SIGPLAN notices. 2010, Vol 45, Num 6, pp 99-110, 12 p ; ref : 20 ref
- ISSN
- 1523-2867
- Scientific domain
- Computer science
- Publisher
- Association for Computing Machinery, New York, NY
- Publication country
- United States
- Document type
- Conference Paper
- Language
- English
- Author keyword
- Operating system Verification run-time system type safety verification
- Keyword (fr)
- Durée fonctionnement Démonstration automatique Démonstration théorème Gestion mémoire Langage assembleur Langage typé Logique Hoare Préemption Qualité service Ramasse-miettes Système exploitation Sécurité Théorie preuve Vérification programme
- Keyword (en)
- Operating time Automatic proving Theorem proving Storage management Assembler Typed language Hoare logic Preemption Service quality Garbage collector Operating system Safety Proof theory Program verification
- Keyword (es)
- Duracion funcionamiento Demostración automática Demostración teorema Gestión memoria Lenguaje ensamblador Lenguaje tipado Lógica Hoare Preempción Calidad servicio Recogemigas Sistema operativo Seguridad Teoría demonstración Verificación programa
- Classification
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D02 Computer science; control theory; systems / 001D02B Software / 001D02B02 Programming languages
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D02 Computer science; control theory; systems / 001D02B Software / 001D02B03 Language processing and microprogramming
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D02 Computer science; control theory; systems / 001D02B Software / 001D02B09 Software engineering
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D02 Computer science; control theory; systems / 001D02B Software / 001D02B10 Computer systems performance. Reliability
- Discipline
- Computer science : theoretical automation and systems
- Origin
- Inist-CNRS
- Database
- PASCAL
- INIST identifier
- 23348125
Sauf mention contraire ci-dessus, le contenu de cette notice bibliographique peut être utilisé dans le cadre d’une licence CC BY 4.0 Inist-CNRS / Unless otherwise stated above, the content of this bibliographic record may be used under a CC BY 4.0 licence by Inist-CNRS / A menos que se haya señalado antes, el contenido de este registro bibliográfico puede ser utilizado al amparo de una licencia CC BY 4.0 Inist-CNRS
Install on your browser
