{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,5]],"date-time":"2024-09-05T17:30:19Z","timestamp":1725557419877},"publisher-location":"Berlin, Heidelberg","reference-count":18,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642135552"},{"type":"electronic","value":"9783642135569"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2010]]},"DOI":"10.1007\/978-3-642-13556-9_5","type":"book-chapter","created":{"date-parts":[[2010,6,5]],"date-time":"2010-06-05T05:46:54Z","timestamp":1275716814000},"page":"72-88","source":"Crossref","is-referenced-by-count":0,"title":["A Road to a Formally Verified General-Purpose Operating System"],"prefix":"10.1007","author":[{"given":"Martin","family":"D\u011bck\u00fd","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"issue":"2","key":"5_CR1","doi-asserted-by":"publisher","first-page":"66","DOI":"10.1145\/1646353.1646374","volume":"53","author":"A. Bessey","year":"2010","unstructured":"Bessey, A., Block, K., Chelf, B., Chou, A., Fulton, B., Hallem, S., Henri-Gros, C., Kamsky, A., McPeak, S., Engler, D.: A Few Billion Lines of Code Later: Using Static Analysis to Find Bugs in the Real World. Communications of the ACM\u00a053(2), 66\u201375 (2010)","journal-title":"Communications of the ACM"},{"key":"5_CR2","doi-asserted-by":"crossref","unstructured":"Kofron, J.: Checking Software Component Behavior Using Behavior Protocols and Spin. In: Proceedings of Applied Computing 2007, Seoul, Korea, pp. 1513\u20131517 (2007)","DOI":"10.1145\/1244002.1244326"},{"key":"5_CR3","unstructured":"GCC, the GNU Compiler Collection, \n                    \n                      http:\/\/gcc.gnu.org\/"},{"key":"5_CR4","unstructured":"Clang: a C language family frontend for LLVM, \n                    \n                      http:\/\/clang.llvm.org\/"},{"key":"5_CR5","unstructured":"Clang Static Analyzer, \n                    \n                      http:\/\/clang-analyzer.llvm.org\/"},{"key":"5_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"357","DOI":"10.1007\/978-3-540-85289-6_14","volume-title":"The Common Component Modeling Example","author":"L. Bulej","year":"2008","unstructured":"Bulej, L., Bures, T., Coupaye, T., Decky, M., Jezek, P., Parizek, P., Plasil, F., Poch, T., Rivierre, N., Sery, O., Tuma, P.: CoCoME in Fractal. In: Rausch, A., Reussner, R., Mirandola, R., Pl\u00e1\u0161il, F. (eds.) The Common Component Modeling Example. LNCS, vol.\u00a05153, pp. 357\u2013387. Springer, Heidelberg (2008)"},{"key":"5_CR7","unstructured":"Coverity, \n                    \n                      http:\/\/scan.coverity.com\/"},{"key":"5_CR8","unstructured":"Mencl, V.: Deriving Behavior Specifications from Textual Use Cases. In: Proceedings of Workshop on Intelligent Technologies for Software Engineering (WITSE 2004), Linz, Austria, September 21, part of ASE 2004, pp. 331\u2013341. Oesterreichische Computer Gesellschaft (2004)"},{"key":"5_CR9","unstructured":"Frama-C, \n                    \n                      http:\/\/frama-c.cea.fr\/"},{"key":"5_CR10","unstructured":"Lawlis, P.K.: Guidelines for Choosing a Computer Language: Support for the Visionary Organization. Ada Information Clearinghouse (1998), \n                    \n                      http:\/\/archive.adaic.com\/docs\/reports\/lawlis\/k.htm"},{"key":"5_CR11","unstructured":"HelenOS Project, \n                    \n                      http:\/\/www.helenos.org\/"},{"key":"5_CR12","unstructured":"Oplustil, T.: Inheritance in Architecture Description Languages. In: Reviewed section of Proceedings of the Week of Doctoral Students 2003 conference (WDS 2003), Charles University, Prague, Czech Republic, vol.\u00a02003, pp. 124\u2013131 (2003)"},{"key":"5_CR13","unstructured":"Operating System Market Share, \n                    \n                      http:\/\/marketshare.hitslink.com\/report.aspx?qprid=8&qptimeframe=M&qpsp=132\n                    \n                    \n                   (retrieved on 2010-02-28)"},{"key":"5_CR14","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., Andronick, J., Cock, D., Derrin, P., Elkaduwe, D., Engelhardt, K., Kolanski, R., Norrish, M., Sewell, T., Tuch, H., Winwood, S.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA (2009)","DOI":"10.1145\/1629575.1629596"},{"key":"5_CR15","unstructured":"Spin, \n                    \n                      http:\/\/spinroot.com\/"},{"key":"5_CR16","unstructured":"Stanse: Static Analysis Framework for C code, \n                    \n                      http:\/\/stanse.fi.muni.cz\/"},{"key":"5_CR17","unstructured":"Valgrind, \n                    \n                      http:\/\/valgrind.org\/"},{"key":"5_CR18","unstructured":"VCC, \n                    \n                      http:\/\/vcc.codeplex.com\/"}],"container-title":["Lecture Notes in Computer Science","Architecting Critical Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-13556-9_5.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,4,30]],"date-time":"2021-04-30T12:07:16Z","timestamp":1619784436000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-13556-9_5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2010]]},"ISBN":["9783642135552","9783642135569"],"references-count":18,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-13556-9_5","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2010]]}}}