Comprehensive Formal Verification of an OS Microkernel
- Author
- KLEIN, Gerwin1 ; ANDRONICK, June1 ; ELPHINSTONE, Kevin1 ; MURRAY, Toby1 ; SEWELL, Thomas1 ; KOLANSKI, Rafal1 ; HEISER, Gernot1
[1] NICTA and UNSW, Sydney, Australia - Source
ACM transactions on computer systems. 2014, Vol 32, Num 1 ; 2.1-2.70 ; ref : 6 p
- CODEN
- ACSYEC
- ISSN
- 0734-2071
- Scientific domain
- Electronics; Computer science; Telecommunications
- Publisher
- Association for Computing Machinery, New York, NY
- Publication country
- United States
- Document type
- Article
- Language
- English
- Author keyword
- Isabelle/HOL L4 Reliability Security Verification microkernel operating systems seL4
- Keyword (fr)
- Analyse temporelle Codage Code binaire Contrôle accès Couverture Fiabilité Flux information Implémentation Méthode cas pire Méthode noyau Signal audio Système expert Système exploitation Sécurité Sémantique Temps exécution Vérification formelle Signal acoustique
- Keyword (en)
- Time analysis Coding Binary code Access control Coverage Reliability Information flow Implementation Worst case method Kernel method Audio signal Expert system Operating system Safety Semantics Execution time Formal verification Acoustic signal
- Keyword (es)
- Análisis temporal Codificación Código binario Cobertura Fiabilidad Flujo información Implementación Método caso peor Método núcleo Señal audio Sistema experto Sistema operativo Seguridad Semántica Tiempo ejecución Señal acústica
- Classification
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D02 Computer science; control theory; systems / 001D02B Software / 001D02B04 Computer systems and distributed systems. User interface
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D04 Telecommunications and information theory / 001D04A Information, signal and communications theory / 001D04A04 Signal and communications theory / 001D04A04B Coding, codes
- Pascal
- 001 Exact sciences and technology / 001D Applied sciences / 001D04 Telecommunications and information theory / 001D04B Telecommunications / 001D04B03 Teleprocessing networks. Isdn / 001D04B03A Access methods and protocols, osi model
- Discipline
- Computer science : theoretical automation and systems Telecommunications and information theory
- Origin
- Inist-CNRS
- Database
- PASCAL
- INIST identifier
- 28323862
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
Access to the document
Install on your browser
DOI
10.1145/2560537 
https://dx.doi.org/10.1145/2560537
"O:13:\"PanistOpenUrl\":36:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000idc\";N;s:6:\"\u0000*\u0000fmt\";s:7:\"journal\";s:6:\"\u0000*\u0000doi\";s:15:\"10.1145\/2560537\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";s:9:\"\u0000*\u0000jtitle\";s:36:\"ACM transactions on computer systems\";s:9:\"\u0000*\u0000stitle\";s:23:\"ACM trans. comput. syst\";s:7:\"\u0000*\u0000date\";s:4:\"2014\";s:9:\"\u0000*\u0000volume\";s:2:\"32\";s:8:\"\u0000*\u0000issue\";s:1:\"1\";s:8:\"\u0000*\u0000spage\";s:0:\"\";s:8:\"\u0000*\u0000epage\";s:0:\"\";s:8:\"\u0000*\u0000pages\";s:8:\"2.1-2.70\";s:7:\"\u0000*\u0000issn\";s:9:\"0734-2071\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:5:\"KLEIN\";s:10:\"\u0000*\u0000aufirst\";s:6:\"Gerwin\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:6:{i:0;s:15:\"ANDRONICK, June\";i:1;s:18:\"ELPHINSTONE, Kevin\";i:2;s:12:\"MURRAY, Toby\";i:3;s:14:\"SEWELL, Thomas\";i:4;s:15:\"KOLANSKI, Rafal\";i:5;s:14:\"HEISER, Gernot\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:6:\"ACSYEC\";s:8:\"\u0000*\u0000genre\";s:7:\"article\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:0:\"\";s:8:\"\u0000*\u0000title\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";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:0:\"\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Panist access
"O:12:\"IstexOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:7:\"journal\";s:6:\"\u0000*\u0000doi\";s:15:\"10.1145\/2560537\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";s:9:\"\u0000*\u0000jtitle\";s:36:\"ACM transactions on computer systems\";s:9:\"\u0000*\u0000stitle\";s:23:\"ACM trans. comput. syst\";s:7:\"\u0000*\u0000date\";s:4:\"2014\";s:9:\"\u0000*\u0000volume\";s:2:\"32\";s:8:\"\u0000*\u0000issue\";s:1:\"1\";s:8:\"\u0000*\u0000spage\";s:0:\"\";s:8:\"\u0000*\u0000epage\";s:0:\"\";s:8:\"\u0000*\u0000pages\";s:8:\"2.1-2.70\";s:7:\"\u0000*\u0000issn\";s:9:\"0734-2071\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:5:\"KLEIN\";s:10:\"\u0000*\u0000aufirst\";s:6:\"Gerwin\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:6:{i:0;s:15:\"ANDRONICK, June\";i:1;s:18:\"ELPHINSTONE, Kevin\";i:2;s:12:\"MURRAY, Toby\";i:3;s:14:\"SEWELL, Thomas\";i:4;s:15:\"KOLANSKI, Rafal\";i:5;s:14:\"HEISER, Gernot\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:6:\"ACSYEC\";s:8:\"\u0000*\u0000genre\";s:7:\"article\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:0:\"\";s:8:\"\u0000*\u0000title\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";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:0:\"\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Istex access
"O:16:\"UnpaywallOpenUrl\":35:{s:8:\"\u0000*\u0000email\";s:27:\"assistance-portail@inist.fr\";s:6:\"\u0000*\u0000fmt\";N;s:6:\"\u0000*\u0000doi\";s:15:\"10.1145\/2560537\";s:6:\"\u0000*\u0000pii\";N;s:7:\"\u0000*\u0000pmid\";N;s:9:\"\u0000*\u0000atitle\";N;s:9:\"\u0000*\u0000jtitle\";N;s:9:\"\u0000*\u0000stitle\";N;s:7:\"\u0000*\u0000date\";N;s:9:\"\u0000*\u0000volume\";N;s:8:\"\u0000*\u0000issue\";N;s:8:\"\u0000*\u0000spage\";N;s:8:\"\u0000*\u0000epage\";N;s:8:\"\u0000*\u0000pages\";N;s:7:\"\u0000*\u0000issn\";N;s:8:\"\u0000*\u0000eissn\";N;s:9:\"\u0000*\u0000aulast\";N;s:10:\"\u0000*\u0000aufirst\";N;s:9:\"\u0000*\u0000auinit\";N;s:10:\"\u0000*\u0000auinitm\";N;s:5:\"\u0000*\u0000au\";N;s:9:\"\u0000*\u0000aucorp\";N;s:7:\"\u0000*\u0000isbn\";N;s:8:\"\u0000*\u0000coden\";N;s:8:\"\u0000*\u0000genre\";N;s:7:\"\u0000*\u0000part\";N;s:9:\"\u0000*\u0000btitle\";N;s:8:\"\u0000*\u0000title\";N;s:8:\"\u0000*\u0000place\";N;s:6:\"\u0000*\u0000pub\";N;s:10:\"\u0000*\u0000edition\";N;s:9:\"\u0000*\u0000tpages\";N;s:9:\"\u0000*\u0000series\";N;s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";N;}"
Unpaywall access
"O:16:\"EuropePMCOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:7:\"journal\";s:6:\"\u0000*\u0000doi\";s:15:\"10.1145\/2560537\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";s:9:\"\u0000*\u0000jtitle\";s:36:\"ACM transactions on computer systems\";s:9:\"\u0000*\u0000stitle\";s:23:\"ACM trans. comput. syst\";s:7:\"\u0000*\u0000date\";s:4:\"2014\";s:9:\"\u0000*\u0000volume\";s:2:\"32\";s:8:\"\u0000*\u0000issue\";s:1:\"1\";s:8:\"\u0000*\u0000spage\";s:0:\"\";s:8:\"\u0000*\u0000epage\";s:0:\"\";s:8:\"\u0000*\u0000pages\";s:8:\"2.1-2.70\";s:7:\"\u0000*\u0000issn\";s:9:\"0734-2071\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:5:\"KLEIN\";s:10:\"\u0000*\u0000aufirst\";s:6:\"Gerwin\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:6:{i:0;s:15:\"ANDRONICK, June\";i:1;s:18:\"ELPHINSTONE, Kevin\";i:2;s:12:\"MURRAY, Toby\";i:3;s:14:\"SEWELL, Thomas\";i:4;s:15:\"KOLANSKI, Rafal\";i:5;s:14:\"HEISER, Gernot\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:6:\"ACSYEC\";s:8:\"\u0000*\u0000genre\";s:7:\"article\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:0:\"\";s:8:\"\u0000*\u0000title\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";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:0:\"\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Europe PubMed Central access
"O:11:\"BaseOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:7:\"journal\";s:6:\"\u0000*\u0000doi\";s:15:\"10.1145\/2560537\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";s:9:\"\u0000*\u0000jtitle\";s:36:\"ACM transactions on computer systems\";s:9:\"\u0000*\u0000stitle\";s:23:\"ACM trans. comput. syst\";s:7:\"\u0000*\u0000date\";s:4:\"2014\";s:9:\"\u0000*\u0000volume\";s:2:\"32\";s:8:\"\u0000*\u0000issue\";s:1:\"1\";s:8:\"\u0000*\u0000spage\";s:0:\"\";s:8:\"\u0000*\u0000epage\";s:0:\"\";s:8:\"\u0000*\u0000pages\";s:8:\"2.1-2.70\";s:7:\"\u0000*\u0000issn\";s:9:\"0734-2071\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:5:\"KLEIN\";s:10:\"\u0000*\u0000aufirst\";s:6:\"Gerwin\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:6:{i:0;s:15:\"ANDRONICK, June\";i:1;s:18:\"ELPHINSTONE, Kevin\";i:2;s:12:\"MURRAY, Toby\";i:3;s:14:\"SEWELL, Thomas\";i:4;s:15:\"KOLANSKI, Rafal\";i:5;s:14:\"HEISER, Gernot\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:6:\"ACSYEC\";s:8:\"\u0000*\u0000genre\";s:7:\"article\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:0:\"\";s:8:\"\u0000*\u0000title\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";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:0:\"\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
Base Search access
"O:12:\"ArXivOpenUrl\":35:{s:10:\"\u0000*\u0000openUrl\";N;s:6:\"\u0000*\u0000fmt\";s:7:\"journal\";s:6:\"\u0000*\u0000doi\";s:15:\"10.1145\/2560537\";s:6:\"\u0000*\u0000pii\";s:0:\"\";s:7:\"\u0000*\u0000pmid\";s:0:\"\";s:9:\"\u0000*\u0000atitle\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";s:9:\"\u0000*\u0000jtitle\";s:36:\"ACM transactions on computer systems\";s:9:\"\u0000*\u0000stitle\";s:23:\"ACM trans. comput. syst\";s:7:\"\u0000*\u0000date\";s:4:\"2014\";s:9:\"\u0000*\u0000volume\";s:2:\"32\";s:8:\"\u0000*\u0000issue\";s:1:\"1\";s:8:\"\u0000*\u0000spage\";s:0:\"\";s:8:\"\u0000*\u0000epage\";s:0:\"\";s:8:\"\u0000*\u0000pages\";s:8:\"2.1-2.70\";s:7:\"\u0000*\u0000issn\";s:9:\"0734-2071\";s:8:\"\u0000*\u0000eissn\";s:0:\"\";s:9:\"\u0000*\u0000aulast\";s:5:\"KLEIN\";s:10:\"\u0000*\u0000aufirst\";s:6:\"Gerwin\";s:9:\"\u0000*\u0000auinit\";s:0:\"\";s:10:\"\u0000*\u0000auinitm\";s:0:\"\";s:5:\"\u0000*\u0000au\";a:6:{i:0;s:15:\"ANDRONICK, June\";i:1;s:18:\"ELPHINSTONE, Kevin\";i:2;s:12:\"MURRAY, Toby\";i:3;s:14:\"SEWELL, Thomas\";i:4;s:15:\"KOLANSKI, Rafal\";i:5;s:14:\"HEISER, Gernot\";}s:9:\"\u0000*\u0000aucorp\";s:0:\"\";s:7:\"\u0000*\u0000isbn\";s:0:\"\";s:8:\"\u0000*\u0000coden\";s:6:\"ACSYEC\";s:8:\"\u0000*\u0000genre\";s:7:\"article\";s:7:\"\u0000*\u0000part\";s:0:\"\";s:9:\"\u0000*\u0000btitle\";s:0:\"\";s:8:\"\u0000*\u0000title\";s:54:\"Comprehensive Formal Verification of an OS Microkernel\";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:0:\"\";s:9:\"\u0000*\u0000series\";s:0:\"\";s:8:\"\u0000*\u0000proxy\";s:30:\"http:\/\/proxyout.inist.fr:8080\/\";s:12:\"\u0000*\u0000integrite\";b:1;}"
arXiv access
