{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T00:17:13Z","timestamp":1740097033823,"version":"3.37.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319061993"},{"type":"electronic","value":"9783319062006"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2014]]},"DOI":"10.1007\/978-3-319-06200-6_12","type":"book-chapter","created":{"date-parts":[[2014,4,23]],"date-time":"2014-04-23T01:53:48Z","timestamp":1398218028000},"page":"158-172","source":"Crossref","is-referenced-by-count":0,"title":["Using Lightweight Theorem Proving in an Asynchronous Systems Context"],"prefix":"10.1007","author":[{"given":"Matthew","family":"Danish","sequence":"first","affiliation":[]},{"given":"Hongwei","family":"Xi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-540-87873-5_18","volume-title":"Verified Software: Theories, Tools, Experiments","author":"E. Alkassar","year":"2008","unstructured":"Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A.: The Verisoft Approach to Systems Verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol.\u00a05295, pp. 209\u2013224. Springer, Heidelberg (2008)"},{"key":"12_CR2","unstructured":"ARM Limited. ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition (2011)"},{"key":"12_CR3","doi-asserted-by":"crossref","unstructured":"Bershad, B.N., Savage, S., Pardyak, P., Sirer, E.G., Fiuczynski, M., Becker, D., Eggers, S., Chambers, C.: Extensibility, Safety and Performance in the SPIN Operating System. In: Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles, pp. 267\u2013284 (1995)","DOI":"10.1145\/224056.224077"},{"key":"12_CR4","unstructured":"Blume, M., et al.: Standard ML of New Jersey (2009), \n                  \n                    http:\/\/www.smlnj.org\/"},{"key":"12_CR5","unstructured":"Cardelli, L., et al.: Modula-3 report (revised). Technical report, Digital Equipment Corp. (now HP Inc.) (November 1989), \n                  \n                    http:\/\/www.hpl.hp.com\/techreports\/Compaq-DEC\/SRC-RR-52.html"},{"key":"12_CR6","doi-asserted-by":"crossref","unstructured":"Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ICFP 2005: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pp. 66\u201377. ACM Press (2005)","DOI":"10.1145\/1090189.1086375"},{"key":"12_CR7","unstructured":"Danish, M.: Terrier OS, \n                  \n                    http:\/\/www.github.com\/mrd\/terrier"},{"key":"12_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L. Moura de","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol.\u00a04963, pp. 337\u2013340. Springer, Heidelberg (2008)"},{"key":"12_CR9","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/2517349.2522720","volume-title":"Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP 2013","author":"K. Elphinstone","year":"2013","unstructured":"Elphinstone, K., Heiser, G.: From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels? In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP 2013, pp. 133\u2013150. ACM, New York (2013)"},{"key":"12_CR10","unstructured":"Fu, G.: Design and Implementation of an Operating System in Standard ML. Master\u2019s thesis, University of Hawaii (August 1999), \n                  \n                    http:\/\/www2.hawaii.edu\/~esb\/prof\/proj\/hello\/"},{"issue":"9","key":"12_CR11","doi-asserted-by":"publisher","first-page":"116","DOI":"10.1145\/1090189.1086380","volume":"40","author":"T. Hallgren","year":"2005","unstructured":"Hallgren, T., Jones, M.P., Leslie, R., Tolmach, A.: A principled approach to operating system construction in Haskell. SIGPLAN Not.\u00a040(9), 116\u2013128 (2005)","journal-title":"SIGPLAN Not."},{"key":"12_CR12","volume-title":"The formal classification and verification of Simpson\u2019s 4-slot asynchronous communication mechanism","author":"N. Henderson","year":"2002","unstructured":"Henderson, N., Paynter, S.E.: The formal classification and verification of Simpson\u2019s 4-slot asynchronous communication mechanism. Springer, Heidelberg (2002)"},{"key":"12_CR13","unstructured":"Hohmuth, M., Tews, H.: The VFiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems (2005), \n                  \n                    http:\/\/www.cs.ru.nl\/H.Tews\/Plos-2005\/ecoop-plos-05-letter.pdf"},{"key":"12_CR14","doi-asserted-by":"crossref","unstructured":"Hunt, G.C., Laru, J.R.: Singularity: Rethinking the Software Stack. In: ACM SIGOPS Operating System Review, vol.\u00a041, pp. 37\u201349. Association for Computing Machinery (April 2007)","DOI":"10.1145\/1243418.1243424"},{"key":"12_CR15","doi-asserted-by":"crossref","unstructured":"Klein, G., Elphinstone, K., Heiser, G., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA (October 2009)","DOI":"10.1145\/1629575.1629596"},{"key":"12_CR16","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1007\/BF01786227","volume":"1-2","author":"L. Lamport","year":"1986","unstructured":"Lamport, L.: On interprocess communication. Distributed Computing\u00a01-2, 77\u2013101 (1986)","journal-title":"Distributed Computing"},{"key":"12_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle","author":"L.C. Paulson","year":"1994","unstructured":"Paulson, L.C.: Isabelle. LNCS, vol.\u00a0828. Springer, Heidelberg (1994)"},{"key":"12_CR18","unstructured":"Peyton-Jones, S., Marlow, S., et al.: The Glasgow Haskell Compiler, \n                  \n                    http:\/\/www.haskell.org\/ghc\/"},{"key":"12_CR19","unstructured":"Rushby, J.: Model checking Simpson\u2019s four-slot fully asynchronous communication mechanism. Computer Science Laboratory\u2013SRI International, Tech. Rep. Issued (2002)"},{"key":"12_CR20","doi-asserted-by":"crossref","unstructured":"Simpson, H.R.: Four-slot fully asynchronous communication mechanism. In: IEE Proceedings, vol.\u00a0137, Pt. E, No. 1. IEE (January 1990)","DOI":"10.1049\/ip-e.1990.0002"},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1049\/ip-e.1992.0006","volume":"139","author":"H.R. Simpson","year":"1992","unstructured":"Simpson, H.R.: Correctness analysis for class of asynchronous communication mechanisms. IEE Proceedings E (Computers and Digital Techniques)\u00a0139, 35\u201349 (1992)","journal-title":"IEE Proceedings E (Computers and Digital Techniques)"},{"key":"12_CR22","doi-asserted-by":"crossref","unstructured":"Simpson, H.R.: Role model analysis of an asynchronous communication mechanism. In: Computers and Digital Techniques, IEE Proceedings, vol.\u00a0144, pp. 232\u2013240. IET (1997)","DOI":"10.1049\/ip-cdt:19971219"},{"key":"12_CR23","unstructured":"Torvalds, L., et al.: Linux, \n                  \n                    http:\/\/www.linuxfoundation.org\/"},{"key":"12_CR24","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1007\/3-540-57182-5_12","volume-title":"Mathematical Foundations of Computer Science 1993","author":"P. Wadler","year":"1993","unstructured":"Wadler, P.: A taste of linear logic. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol.\u00a0711, pp. 185\u2013210. Springer, Heidelberg (1993), \n                  \n                    http:\/\/dx.doi.org\/10.1007\/3-540-57182-5_12"},{"key":"12_CR25","unstructured":"Xi, H., et al.: The ATS language, \n                  \n                    http:\/\/www.ats-lang.org\/"},{"key":"12_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-540-30557-6_8","volume-title":"Practical Aspects of Declarative Languages","author":"D. Zhu","year":"2005","unstructured":"Zhu, D., Xi, H.: Safe Programming with Pointers through Stateful Views. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol.\u00a03350, pp. 83\u201397. Springer, Heidelberg (2005)"}],"container-title":["Lecture Notes in Computer Science","NASA Formal Methods"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-06200-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,26]],"date-time":"2019-05-26T13:24:30Z","timestamp":1558877070000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-06200-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014]]},"ISBN":["9783319061993","9783319062006"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-06200-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2014]]}}}