Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System
- Autor
- YANG, Jean1 ; HAWBLITZEL, Chris2
[1] Massachusetts Institute of Technology, United States
[2] Microsoft Research, United States - Titulo de la conferencia
- Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)
- Nombre de la conferencia
- ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10) (PLDI'10) (Toronto, Ontario 2010-06-05)
- Autor ( monografía)
- 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) - Fuente
ACM SIGPLAN notices. 2010, Vol 45, Num 6, pp 99-110, 12 p ; ref : 20 ref
- ISSN
- 1523-2867
- Campo Científico
- Computer science
- Editor
- Association for Computing Machinery, New York, NY
- País de la publicación
- United States
- Tipo de documento
- Conference Paper
- Idioma
- English
- Palabra clave de autor
- Operating system Verification run-time system type safety verification
- Palabra clave (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
- Palabra clave (in)
- 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
- Palabra clave (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
- Clasificación
- 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
- Disciplina
- Computer science : theoretical automation and systems
- Procedencia
- Inist-CNRS
- Base de datos
- PASCAL
- Identificador INIST
- 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
"O:13:\"PanistOpenUrl\":36:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000idc\";N;s:6:\"\u0000*\u0000fmt\";s:10:\"proceeding\";s:6:\"\u0000*\u0000doi\";s:0:\"\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:9:\"\u0000*\u0000jtitle\";s:19:\"ACM SIGPLAN notices\";s:9:\"\u0000*\u0000stitle\";s:15:\"ACM SIGPLAN not\";s:7:\"\u0000*\u0000date\";s:4:\"2010\";s:9:\"\u0000*\u0000volume\";s:2:\"45\";s:8:\"\u0000*\u0000issue\";s:1:\"6\";s:8:\"\u0000*\u0000spage\";s:2:\"99\";s:8:\"\u0000*\u0000epage\";s:3:\"110\";s:8:\"\u0000*\u0000pages\";s:0:\"\";s:7:\"\u0000*\u0000issn\";s:9:\"1523-2867\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:4:\"YANG\";s:10:\"\u0000*\u0000aufirst\";s:4:\"Jean\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:1:{i:0;s:17:\"HAWBLITZEL, Chris\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:0:\"\";s:8:\"\u0000*\u0000genre\";s:10:\"proceeding\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:106:\"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)\";s:8:\"\u0000*\u0000title\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:8:\"\u0000*\u0000place\";s:12:\"New York, NY\";s:6:\"\u0000*\u0000pub\";s:35:\"Association for Computing Machinery\";s:10:\"\u0000*\u0000edition\";s:0:\"\";s:9:\"\u0000*\u0000tpages\";s:2:\"12\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Acceso mediante Panist
"O:12:\"IstexOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:10:\"proceeding\";s:6:\"\u0000*\u0000doi\";s:0:\"\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:9:\"\u0000*\u0000jtitle\";s:19:\"ACM SIGPLAN notices\";s:9:\"\u0000*\u0000stitle\";s:15:\"ACM SIGPLAN not\";s:7:\"\u0000*\u0000date\";s:4:\"2010\";s:9:\"\u0000*\u0000volume\";s:2:\"45\";s:8:\"\u0000*\u0000issue\";s:1:\"6\";s:8:\"\u0000*\u0000spage\";s:2:\"99\";s:8:\"\u0000*\u0000epage\";s:3:\"110\";s:8:\"\u0000*\u0000pages\";s:0:\"\";s:7:\"\u0000*\u0000issn\";s:9:\"1523-2867\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:4:\"YANG\";s:10:\"\u0000*\u0000aufirst\";s:4:\"Jean\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:1:{i:0;s:17:\"HAWBLITZEL, Chris\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:0:\"\";s:8:\"\u0000*\u0000genre\";s:10:\"proceeding\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:106:\"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)\";s:8:\"\u0000*\u0000title\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:8:\"\u0000*\u0000place\";s:12:\"New York, NY\";s:6:\"\u0000*\u0000pub\";s:35:\"Association for Computing Machinery\";s:10:\"\u0000*\u0000edition\";s:0:\"\";s:9:\"\u0000*\u0000tpages\";s:2:\"12\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Acceso mediante Istex
"O:16:\"EuropePMCOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:10:\"proceeding\";s:6:\"\u0000*\u0000doi\";s:0:\"\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:9:\"\u0000*\u0000jtitle\";s:19:\"ACM SIGPLAN notices\";s:9:\"\u0000*\u0000stitle\";s:15:\"ACM SIGPLAN not\";s:7:\"\u0000*\u0000date\";s:4:\"2010\";s:9:\"\u0000*\u0000volume\";s:2:\"45\";s:8:\"\u0000*\u0000issue\";s:1:\"6\";s:8:\"\u0000*\u0000spage\";s:2:\"99\";s:8:\"\u0000*\u0000epage\";s:3:\"110\";s:8:\"\u0000*\u0000pages\";s:0:\"\";s:7:\"\u0000*\u0000issn\";s:9:\"1523-2867\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:4:\"YANG\";s:10:\"\u0000*\u0000aufirst\";s:4:\"Jean\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:1:{i:0;s:17:\"HAWBLITZEL, Chris\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:0:\"\";s:8:\"\u0000*\u0000genre\";s:10:\"proceeding\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:106:\"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)\";s:8:\"\u0000*\u0000title\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:8:\"\u0000*\u0000place\";s:12:\"New York, NY\";s:6:\"\u0000*\u0000pub\";s:35:\"Association for Computing Machinery\";s:10:\"\u0000*\u0000edition\";s:0:\"\";s:9:\"\u0000*\u0000tpages\";s:2:\"12\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Acceso mediante Europe PubMed Central
"O:11:\"BaseOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:10:\"proceeding\";s:6:\"\u0000*\u0000doi\";s:0:\"\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:9:\"\u0000*\u0000jtitle\";s:19:\"ACM SIGPLAN notices\";s:9:\"\u0000*\u0000stitle\";s:15:\"ACM SIGPLAN not\";s:7:\"\u0000*\u0000date\";s:4:\"2010\";s:9:\"\u0000*\u0000volume\";s:2:\"45\";s:8:\"\u0000*\u0000issue\";s:1:\"6\";s:8:\"\u0000*\u0000spage\";s:2:\"99\";s:8:\"\u0000*\u0000epage\";s:3:\"110\";s:8:\"\u0000*\u0000pages\";s:0:\"\";s:7:\"\u0000*\u0000issn\";s:9:\"1523-2867\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:4:\"YANG\";s:10:\"\u0000*\u0000aufirst\";s:4:\"Jean\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:1:{i:0;s:17:\"HAWBLITZEL, Chris\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:0:\"\";s:8:\"\u0000*\u0000genre\";s:10:\"proceeding\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:106:\"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)\";s:8:\"\u0000*\u0000title\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:8:\"\u0000*\u0000place\";s:12:\"New York, NY\";s:6:\"\u0000*\u0000pub\";s:35:\"Association for Computing Machinery\";s:10:\"\u0000*\u0000edition\";s:0:\"\";s:9:\"\u0000*\u0000tpages\";s:2:\"12\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Acceso mediante Base Search
"O:12:\"ArXivOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:10:\"proceeding\";s:6:\"\u0000*\u0000doi\";s:0:\"\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:9:\"\u0000*\u0000jtitle\";s:19:\"ACM SIGPLAN notices\";s:9:\"\u0000*\u0000stitle\";s:15:\"ACM SIGPLAN not\";s:7:\"\u0000*\u0000date\";s:4:\"2010\";s:9:\"\u0000*\u0000volume\";s:2:\"45\";s:8:\"\u0000*\u0000issue\";s:1:\"6\";s:8:\"\u0000*\u0000spage\";s:2:\"99\";s:8:\"\u0000*\u0000epage\";s:3:\"110\";s:8:\"\u0000*\u0000pages\";s:0:\"\";s:7:\"\u0000*\u0000issn\";s:9:\"1523-2867\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:4:\"YANG\";s:10:\"\u0000*\u0000aufirst\";s:4:\"Jean\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:1:{i:0;s:17:\"HAWBLITZEL, Chris\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:0:\"\";s:8:\"\u0000*\u0000genre\";s:10:\"proceeding\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:106:\"Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'10)\";s:8:\"\u0000*\u0000title\";s:84:\"Safe to the Last Instruction: Automated Verification of a Type-Safe Operating System\";s:8:\"\u0000*\u0000place\";s:12:\"New York, NY\";s:6:\"\u0000*\u0000pub\";s:35:\"Association for Computing Machinery\";s:10:\"\u0000*\u0000edition\";s:0:\"\";s:9:\"\u0000*\u0000tpages\";s:2:\"12\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Acceso mediante arXiv
