{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:47:04Z","timestamp":1725864424842},"publisher-location":"Cham","reference-count":24,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319454764"},{"type":"electronic","value":"9783319454771"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-45477-1_9","type":"book-chapter","created":{"date-parts":[[2016,9,3]],"date-time":"2016-09-03T05:34:41Z","timestamp":1472880881000},"page":"102-113","source":"Crossref","is-referenced-by-count":2,"title":["A High-Assurance, High-Performance Hardware-Based Cross-Domain System"],"prefix":"10.1007","author":[{"given":"David","family":"Hardin","sequence":"first","affiliation":[]},{"given":"Konrad","family":"Slind","sequence":"additional","affiliation":[]},{"given":"Mark","family":"Bortz","sequence":"additional","affiliation":[]},{"given":"James","family":"Potts","sequence":"additional","affiliation":[]},{"given":"Scott","family":"Owens","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2016,9,4]]},"reference":[{"key":"9_CR1","unstructured":"Ada Working Group (ISO WG 9). Ada Reference Manual: Language and Standard Libraries (2012)"},{"key":"9_CR2","doi-asserted-by":"crossref","DOI":"10.1017\/CBO9781107256552","volume-title":"Program Logics for Certified Compilers","author":"AW Appel","year":"2014","unstructured":"Appel, A.W.: Program Logics for Certified Compilers. Cambridge University Press, Cambridge (2014)"},{"key":"9_CR3","volume-title":"High Integrity Software: The SPARK Approach to Safety and Security","author":"J Barnes","year":"2003","unstructured":"Barnes, J.: High Integrity Software: The SPARK Approach to Safety and Security. Addison-Wesley, Boston (2003)"},{"key":"9_CR4","doi-asserted-by":"crossref","unstructured":"Blanc, R., Kuncak, V., Kneuss, E., Suter, P.: An overview of the Leon verification system: verification by translation to recursive functions. In: Proceedings of the 4th Workshop on Scala, SCALA 2013, New York, NY, USA, pp. 1:1\u20131:10. ACM (2013)","DOI":"10.1145\/2489837.2489838"},{"key":"9_CR5","unstructured":"Bortz, M., Wilding, M., Marek, J., Hardin, D., Hiratzka, T.D., Limondin, P.: High-assurance architecture for routing of information between networks of differing security level. United States Patent 8,161,529, April 2012"},{"issue":"4","key":"9_CR6","doi-asserted-by":"crossref","first-page":"481","DOI":"10.1145\/321239.321249","volume":"11","author":"J Brzozowski","year":"1964","unstructured":"Brzozowski, J.: Derivatives of regular expressions. J. ACM 11(4), 481\u2013494 (1964)","journal-title":"J. ACM"},{"key":"9_CR7","doi-asserted-by":"crossref","unstructured":"Eysholdt, M., Behrens, H.: Xtext: implement your language faster than the quick and dirty way. In: Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications Companion, SPLASH 2010, pp. 307\u2013309. ACM (2010)","DOI":"10.1145\/1869542.1869625"},{"key":"9_CR8","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-642-16478-1_2","volume-title":"Implementation and Application of Functional Languages","author":"A Gill","year":"2010","unstructured":"Gill, A., Bull, T., Kimmell, G., Perrins, E., Komp, E., Werling, B.: Introducing Kansas Lava. In: Scholz, S.-B., Moraz\u00e1n, M.T. (eds.) IFL 2009. LNCS, vol. 6041, pp. 18\u201335. Springer, Heidelberg (2010)"},{"key":"9_CR9","doi-asserted-by":"crossref","unstructured":"Greve, D., Slind, K.: A step-indexing approach to partial functions. In: Proceedings of the Eleventh International Workshop on the ACL2 Theorem Prover and its Applications. Electronic Proceedings in Theoretical Computer Science, vol. 114, pp. 42\u201353 (2013)","DOI":"10.4204\/EPTCS.114.4"},{"key":"9_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"18","DOI":"10.1007\/978-3-642-28756-5_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Hardin","year":"2012","unstructured":"Hardin, D., Slind, K., Whalen, M., Pham, T.H.: The Guardol language and verification system. In: Flanagan, C., K\u00f6nig, B. (eds.) TACAS 2012. LNCS, vol. 7214, pp. 18\u201332. Springer, Heidelberg (2012)"},{"key":"9_CR11","unstructured":"Institute of Electrical and Electronics Engineers: IEEE Standard VHDL Language Reference Manual (2000)"},{"key":"9_CR12","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4615-4449-4","volume-title":"Computer-Aided Reasoning: An Approach. Texts and Monographs in Computer Science","author":"M Kaufmann","year":"2000","unstructured":"Kaufmann, M., Manolios, P., Moore, J.S.: Computer-Aided Reasoning: An Approach. Texts and Monographs in Computer Science. Kluwer Academic, Boston (2000)"},{"key":"9_CR13","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL 2014: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 179\u2013191. ACM Press, January 2014","DOI":"10.1145\/2535838.2535841"},{"key":"9_CR14","doi-asserted-by":"crossref","unstructured":"Leino, K. Rustan M.: Developing verified programs with Dafny. In: Proceedings of the International Conference on Software Engineering, ICSE 2013, Piscataway, NJ, USA, pp. 1488\u20131490. IEEE Press (2013)","DOI":"10.1109\/ICSE.2013.6606754"},{"issue":"7","key":"9_CR15","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"9_CR16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/2319.001.0001","volume-title":"The Definition of Standard ML (Revised)","author":"R Milner","year":"1997","unstructured":"Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). The MIT Press, Cambridge (1997)"},{"issue":"2","key":"9_CR17","doi-asserted-by":"crossref","first-page":"173","DOI":"10.1017\/S0956796808007090","volume":"19","author":"S Owens","year":"2009","unstructured":"Owens, S., Reppy, J., Turon, A.: Regular-expression derivatives re-examined. J. Funct. Program. 19(2), 173\u2013190 (2009)","journal-title":"J. Funct. Program."},{"key":"9_CR18","doi-asserted-by":"crossref","unstructured":"Parr, T., Fisher, K.: LL(*): the foundation of the ANTLR parser generator. In: Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2011, pp. 425\u2013436 (2011)","DOI":"10.1145\/1993498.1993548"},{"key":"9_CR19","doi-asserted-by":"crossref","unstructured":"Pham, T.H., Gacek, A., Whalen, M.W.: Reasoning about algebraic data types with abstractions. J. Autom. Reasoning (2016, to appear)","DOI":"10.1007\/s10817-016-9368-2"},{"key":"9_CR20","unstructured":"Rockwell Collins: Rockwell Collins Turnstile Selected for UCDMO\u2019s Baseline List of Validated Cross Domain Products, March 2012"},{"key":"9_CR21","unstructured":"Slind, K., Hardin, D., Davis, J., Owens, S.: Benefits of using logic as an intermediate verification language. In: Review (2016)"},{"key":"9_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008)"},{"key":"9_CR23","doi-asserted-by":"crossref","unstructured":"Tuch, H., Klein, G., Norrish, M.: Types, bytes, and separation logic. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, New York, NY, USA, pp. 97\u2013108, ACM (2007)","DOI":"10.1145\/1190216.1190234"},{"key":"9_CR24","doi-asserted-by":"crossref","first-page":"175","DOI":"10.1007\/978-1-4419-1539-9_6","volume-title":"Design and Verification of Microprocessor Systems for High-Assurance Applications","author":"M Wilding","year":"2010","unstructured":"Wilding, M., Greve, D., Richards, R., Hardin, D.: Formal verification of partition management for the AAMP7G microprocessor. In: Hardin, D. (ed.) Design and Verification of Microprocessor Systems for High-Assurance Applications, pp. 175\u2013192. Springer, New York (2010)"}],"container-title":["Lecture Notes in Computer Science","Computer Safety, Reliability, and Security"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-45477-1_9","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,13]],"date-time":"2019-09-13T05:37:58Z","timestamp":1568353078000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-45477-1_9"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319454764","9783319454771"],"references-count":24,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-45477-1_9","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}